### Nuprl Lemma : quo-lift_wf

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

Proof

Definitions occuring in Statement :  quo-lift: `quo-lift(f)` preima_of_rel: `R_f` equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` prop: `ℙ` infix_ap: `x f y` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` 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` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` prop: `ℙ` subtype_rel: `A ⊆r B` preima_of_rel: `R_f` quo-lift: `quo-lift(f)`
Lemmas referenced :  preima_of_equiv_rel quotient_wf equal-wf-base preima_of_rel_wf equiv_rel_wf quotient-member-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination hypothesis functionExtensionality pointwiseFunctionalityForEquality isectElimination cumulativity sqequalRule lambdaEquality applyEquality independent_isectElimination pertypeElimination productElimination productEquality because_Cache universeEquality functionEquality

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

Date html generated: 2016_10_21-AM-09_44_13
Last ObjectModification: 2016_08_08-PM-09_15_45

Theory : quot_1

Home Index