### Nuprl Lemma : implies-least-equiv

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  R => least-equiv(A;R)`

Proof

Definitions occuring in Statement :  least-equiv: `least-equiv(A;R)` rel_implies: `R1 => R2` uall: `∀[x:A]. B[x]` prop: `ℙ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  infix_ap: `x f y` prop: `ℙ` member: `t ∈ T` least-equiv: `least-equiv(A;R)` implies: `P `` Q` all: `∀x:A. B[x]` rel_implies: `R1 => R2` uall: `∀[x:A]. B[x]` or: `P ∨ Q`
Lemmas referenced :  or_wf transitive-reflexive-closure-base-case
Rules used in proof :  universeEquality functionEquality independent_functionElimination dependent_functionElimination hypothesis cumulativity hypothesisEquality functionExtensionality applyEquality lambdaEquality because_Cache thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution inlFormation sqequalRule

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    R  =>  least-equiv(A;R)

Date html generated: 2018_05_21-PM-00_51_57
Last ObjectModification: 2018_01_08-AM-10_15_33

Theory : relations2

Home Index