### Nuprl Lemma : least-equiv-implies

`∀[A:Type]. ∀[R,E:A ⟶ A ⟶ ℙ].  (R => E `` EquivRel(A;x,y.E x y) `` least-equiv(A;R) => E)`

Proof

Definitions occuring in Statement :  least-equiv: `least-equiv(A;R)` rel_implies: `R1 => R2` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` 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])` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` guard: `{T}` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` member: `t ∈ T` or: `P ∨ Q` infix_ap: `x f y` transitive-reflexive-closure: `R^*` least-equiv: `least-equiv(A;R)` all: `∀x:A. B[x]` rel_implies: `R1 => R2` implies: `P `` Q` uall: `∀[x:A]. B[x]`
Lemmas referenced :  rel_implies_wf equiv_rel_wf least-equiv_wf or_wf transitive-closure-induction iff_weakening_equal
Rules used in proof :  functionEquality cumulativity functionExtensionality because_Cache dependent_functionElimination independent_functionElimination productElimination independent_isectElimination equalitySymmetry equalityTransitivity isectElimination extract_by_obid introduction universeEquality lambdaEquality hypothesis hypothesisEquality applyEquality cut thin unionElimination sqequalRule sqequalHypSubstitution lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution rename

Latex:
\mforall{}[A:Type].  \mforall{}[R,E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (R  =>  E  {}\mRightarrow{}  EquivRel(A;x,y.E  x  y)  {}\mRightarrow{}  least-equiv(A;R)  =>  E)

Date html generated: 2018_05_21-PM-00_51_59
Last ObjectModification: 2018_01_08-AM-10_26_01

Theory : relations2

Home Index