### Nuprl Lemma : quot_elim

`∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (EquivRel(T;x,y.E[x;y]) `` (∀a,b:T.  (a = b ∈ (x,y:T//E[x;y]) `⇐⇒` ↓E[a;b])))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` squash: `↓T` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` squash: `↓T` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` prop: `ℙ` quotient: `x,y:A//B[x; y]` cand: `A c∧ B`
Lemmas referenced :  quotient_wf subtype_quotient squash_wf istype-universe equiv_rel_wf subtype_rel_self quotient-member-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  independent_pairFormation hypothesis sqequalHypSubstitution imageElimination sqequalRule imageMemberEquality hypothesisEquality thin baseClosed Error :equalityIsType1,  Error :universeIsType,  extract_by_obid isectElimination Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  independent_isectElimination dependent_functionElimination productElimination independent_pairEquality Error :functionIsTypeImplies,  axiomEquality Error :functionIsType,  universeEquality Error :isect_memberEquality_alt,  pertypeElimination Error :productIsType,  because_Cache instantiate independent_functionElimination lambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (EquivRel(T;x,y.E[x;y])  {}\mRightarrow{}  (\mforall{}a,b:T.    (a  =  b  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}E[a;b])))

Date html generated: 2019_06_20-PM-00_32_10
Last ObjectModification: 2018_10_06-PM-03_56_26

Theory : quot_1

Home Index