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