### Nuprl Lemma : least-equiv-is-equiv

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

Proof

Definitions occuring in Statement :  least-equiv: `least-equiv(A;R)` equiv_rel: `EquivRel(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` prop: `ℙ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a`
Lemmas referenced :  istype-universe least-equiv-is-equiv-1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt functionIsType universeIsType hypothesisEquality because_Cache universeEquality cut instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality_alt independent_isectElimination

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

Date html generated: 2019_10_15-AM-10_24_57
Last ObjectModification: 2019_08_22-AM-10_52_36

Theory : relations2

Home Index