### Nuprl Lemma : biject-quotient

`∀A,B:Type. ∀f:A ⟶ B. ∀R:B ⟶ B ⟶ ℙ.`
`  (Bij(A;B;f) `` EquivRel(B;x,y.x R y) `` Bij(x,y:A//(x R_f y);x,y:B//(x R y);quo-lift(f)))`

Proof

Definitions occuring in Statement :  quo-lift: `quo-lift(f)` preima_of_rel: `R_f` equiv_rel: `EquivRel(T;x,y.E[x; y])` biject: `Bij(A;B;f)` quotient: `x,y:A//B[x; y]` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` biject: `Bij(A;B;f)` and: `P ∧ Q` cand: `A c∧ B` inject: `Inj(A;B;f)` uall: `∀[x:A]. B[x]` so_lambda: `λ2x y.t[x; y]` infix_ap: `x f y` so_apply: `x[s1;s2]` uimplies: `b supposing a` surject: `Surj(A;B;f)` prop: `ℙ` quotient: `x,y:A//B[x; y]` preima_of_rel: `R_f` subtype_rel: `A ⊆r B` quo-lift: `quo-lift(f)` equiv_rel: `EquivRel(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` exists: `∃x:A. B[x]` pi1: `fst(t)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}`
Lemmas referenced :  preima_of_equiv_rel quo-lift_wf quotient_wf preima_of_rel_wf equiv_rel_wf biject_wf istype-universe infix_ap_wf subtype_rel_self quotient-member-eq iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis because_Cache productElimination Error :equalityIstype,  Error :universeIsType,  isectElimination sqequalRule Error :lambdaEquality_alt,  applyEquality Error :inhabitedIsType,  independent_isectElimination independent_pairFormation Error :functionIsType,  universeEquality instantiate pointwiseFunctionalityForEquality cumulativity pertypeElimination Error :productIsType,  sqequalBase equalitySymmetry equalityTransitivity Error :equalityIsType1,  promote_hyp rename Error :dependent_pairFormation_alt,  functionExtensionality Error :equalityIsType4

Latex:
\mforall{}A,B:Type.  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}.
(Bij(A;B;f)  {}\mRightarrow{}  EquivRel(B;x,y.x  R  y)  {}\mRightarrow{}  Bij(x,y:A//(x  R\_f  y);x,y:B//(x  R  y);quo-lift(f)))

Date html generated: 2019_06_20-PM-00_33_19
Last ObjectModification: 2018_11_24-AM-09_34_34

Theory : quot_1

Home Index