Nuprl Lemma : equipollent-quotient

`∀[A:Type]. ∀E:A ⟶ A ⟶ 𝔹. A ~ a:x,y:A//(↑E[x;y]) × {b:A| ↑E[a;b]}  supposing EquivRel(A;x,y.↑E[x;y])`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` so_apply: `x[s1;s2]` implies: `P `` Q` sym: `Sym(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` guard: `{T}` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` sq_type: `SQType(T)` equipollent: `A ~ B` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` biject: `Bij(A;B;f)` inject: `Inj(A;B;f)` surject: `Surj(A;B;f)` pi2: `snd(t)` squash: `↓T` istype: `istype(T)`
Lemmas referenced :  assert_witness bool_wf iff_imp_equal_bool istype-assert quotient_wf assert_wf equiv_rel_wf istype-universe btrue_wf true_wf subtype_base_sq bool_subtype_base subtype_quotient equal_wf squash_wf quotient-member-eq subtype_rel_self biject_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut introduction sqequalRule sqequalHypSubstitution productElimination thin independent_pairEquality Error :lambdaEquality_alt,  dependent_functionElimination hypothesisEquality extract_by_obid isectElimination applyEquality independent_functionElimination hypothesis Error :functionIsTypeImplies,  Error :inhabitedIsType,  rename Error :functionExtensionality_alt,  pointwiseFunctionalityForEquality functionEquality pertypeElimination promote_hyp because_Cache independent_isectElimination independent_pairFormation equalityTransitivity equalitySymmetry Error :productIsType,  Error :equalityIstype,  sqequalBase Error :universeIsType,  Error :functionIsType,  instantiate universeEquality natural_numberEquality cumulativity Error :dependent_pairFormation_alt,  Error :setIsType,  Error :dependent_set_memberEquality_alt,  Error :dependent_pairEquality_alt,  applyLambdaEquality setElimination pointwiseFunctionality Error :equalityIsType4,  imageElimination imageMemberEquality baseClosed productEquality setEquality

Latex:
\mforall{}[A:Type].  \mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.  A  \msim{}  a:x,y:A//(\muparrow{}E[x;y])  \mtimes{}  \{b:A|  \muparrow{}E[a;b]\}    supposing  EquivRel(A;x,y.\muparrow{}E[x;y]\000C)

Date html generated: 2019_06_20-PM-02_17_35
Last ObjectModification: 2018_11_25-PM-01_28_18

Theory : equipollence!!cardinality!

Home Index