### Nuprl Lemma : equiv_rel_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])))`
`  `` EquivRel(x,y:T//(↑E2[x;y]);x,y.↑E1[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` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` member: `t ∈ T` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` all: `∀x:A. B[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` so_lambda: `λ2x.t[x]` so_apply: `x[s]` quotient: `x,y:A//B[x; y]` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  equiv_rel-wf-quotient quotient_wf assert_wf assert_witness all_wf equiv_rel_wf bool_wf subtype_quotient equal-wf-base equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_functionElimination hypothesis independent_pairFormation cumulativity sqequalRule lambdaEquality applyEquality functionExtensionality independent_isectElimination because_Cache functionEquality universeEquality pointwiseFunctionalityForEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry productEquality dependent_functionElimination rename

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{}  EquivRel(x,y:T//(\muparrow{}E2[x;y]);x,y.\muparrow{}E1[x;y]))

Date html generated: 2017_04_14-AM-07_39_44
Last ObjectModification: 2017_02_27-PM-03_12_30

Theory : quot_1

Home Index