### Nuprl Lemma : equiv_rel-wf-quotient

`∀[T:Type]. ∀[E1,E2:T ⟶ T ⟶ 𝔹].`
`  (EquivRel(T;x,y.↑E2[x;y])`
`  `` EquivRel(T;x,y.↑E1[x;y])`
`  `` (∀x,y:T.  ((↑E2[x;y]) `` (↑E1[x;y])))`
`  `` (E1 ∈ (x,y:T//(↑E2[x;y])) ⟶ (x,y:T//(↑E2[x;y])) ⟶ 𝔹))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` quotient: `x,y:A//B[x; y]` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` so_lambda: `λ2x y.t[x; y]` uimplies: `b supposing a` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` equiv_rel: `EquivRel(T;x,y.E[x; y])` trans: `Trans(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` guard: `{T}`
Lemmas referenced :  all_wf assert_wf equiv_rel_wf bool_wf quotient_wf iff_imp_equal_bool equal_wf equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule lambdaEquality functionEquality applyEquality functionExtensionality hypothesis because_Cache universeEquality pointwiseFunctionalityForEquality independent_isectElimination pertypeElimination productElimination equalityTransitivity equalitySymmetry rename independent_pairFormation dependent_functionElimination independent_functionElimination productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[E1,E2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].
(EquivRel(T;x,y.\muparrow{}E2[x;y])
{}\mRightarrow{}  EquivRel(T;x,y.\muparrow{}E1[x;y])
{}\mRightarrow{}  (\mforall{}x,y:T.    ((\muparrow{}E2[x;y])  {}\mRightarrow{}  (\muparrow{}E1[x;y])))
{}\mRightarrow{}  (E1  \mmember{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  (x,y:T//(\muparrow{}E2[x;y]))  {}\mrightarrow{}  \mBbbB{}))

Date html generated: 2017_04_14-AM-07_39_41
Last ObjectModification: 2017_02_27-PM-03_11_21

Theory : quot_1

Home Index