### Nuprl Lemma : quotient-mono

`∀[T:Type]. (mono(T) `` (∀E:T ⟶ T ⟶ ℙ. (EquivRel(T;x,y.E[x;y]) `` mono(x,y:T//E[x;y]))))`

Proof

Definitions occuring in Statement :  equiv_rel: `EquivRel(T;x,y.E[x; y])` mono: `mono(T)` quotient: `x,y:A//B[x; y]` uall: `∀[x:A]. B[x]` prop: `ℙ` 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]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` mono: `mono(T)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` prop: `ℙ` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` is-above: `is-above(T;a;z)` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` cand: `A c∧ B` trans: `Trans(T;x,y.E[x; y])` sym: `Sym(T;x,y.E[x; y])` refl: `Refl(T;x,y.E[x; y])` equiv_rel: `EquivRel(T;x,y.E[x; y])`
Lemmas referenced :  is-above_wf quotient_wf istype-base equiv_rel_wf mono_wf istype-universe subtype_rel_self sqle_wf_base quotient-member-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut Error :lambdaFormation_alt,  hypothesis Error :universeIsType,  extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule Error :lambdaEquality_alt,  applyEquality because_Cache independent_isectElimination Error :inhabitedIsType,  Error :functionIsType,  universeEquality dependent_functionElimination axiomEquality Error :functionIsTypeImplies,  instantiate pointwiseFunctionalityForEquality pertypeElimination productElimination Error :productIsType,  Error :equalityIstype,  sqequalBase equalitySymmetry equalityTransitivity Error :equalityIsType2,  independent_pairFormation Error :dependent_pairFormation_alt,  independent_functionElimination applyLambdaEquality hyp_replacement

Latex:
\mforall{}[T:Type].  (mono(T)  {}\mRightarrow{}  (\mforall{}E:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (EquivRel(T;x,y.E[x;y])  {}\mRightarrow{}  mono(x,y:T//E[x;y]))))

Date html generated: 2019_06_20-PM-00_32_22
Last ObjectModification: 2018_11_24-AM-09_34_59

Theory : quot_1

Home Index