### Nuprl Lemma : equiv-on-quotient

`∀T:Type. ∀R:T ⟶ T ⟶ ℙ.`
`  (EquivRel(T;x,y.x R y)`
`  `` (∀Q:(x,y:T//(x R y)) ⟶ (x,y:T//(x R y)) ⟶ ℙ. (EquivRel(x,y:T//(x R y);u,v.u Q v) `` EquivRel(T;x,y.x Q y))))`

Proof

Definitions occuring in Statement :  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` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` member: `t ∈ T` subtype_rel: `A ⊆r B` 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` sym: `Sym(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` prop: `ℙ`
Lemmas referenced :  subtype_quotient equiv_rel_wf quotient_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution independent_pairFormation productElimination thin promote_hyp cut hypothesis dependent_functionElimination hypothesisEquality applyEquality introduction extract_by_obid isectElimination sqequalRule lambdaEquality functionExtensionality cumulativity independent_isectElimination because_Cache functionEquality universeEquality

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
(EquivRel(T;x,y.x  R  y)
{}\mRightarrow{}  (\mforall{}Q:(x,y:T//(x  R  y))  {}\mrightarrow{}  (x,y:T//(x  R  y))  {}\mrightarrow{}  \mBbbP{}
(EquivRel(x,y:T//(x  R  y);u,v.u  Q  v)  {}\mRightarrow{}  EquivRel(T;x,y.x  Q  y))))

Date html generated: 2016_10_21-AM-09_44_00
Last ObjectModification: 2016_08_08-PM-08_46_13

Theory : quot_1

Home Index