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

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

Proof

Definitions occuring in Statement :  least-equiv: `least-equiv(A;R)` equiv_rel: `EquivRel(T;x,y.E[x; y])` uimplies: `b supposing a` subtype_rel: `A ⊆r B` 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]` uimplies: `b supposing a` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` or: `P ∨ Q` subtype_rel: `A ⊆r B` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` least-equiv: `least-equiv(A;R)` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` trans: `Trans(T;x,y.E[x; y])` transitive-reflexive-closure: `R^*` transitive-closure: `TC(R)` spreadn: spread3 so_lambda: `λ2x.t[x]` so_apply: `x[s]` rel_path: `rel_path(A;L;x;y)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` pi1: `fst(t)` pi2: `snd(t)` guard: `{T}` append: `as @ bs` infix_ap: `x f y`
Lemmas referenced :  rel_path_wf list_wf subtype_rel_self transitive-reflexive-closure_wf subtype_rel_wf istype-universe transitive-closure_wf reverse_wf or_wf map_wf list_induction all_wf list_ind_nil_lemma istype-void map_nil_lemma reverse_nil_lemma map_cons_lemma reverse-cons list_ind_cons_lemma append_wf cons_wf nil_wf pi1_wf pi2_wf length-reverse length-map istype-less_than length_wf transitive-reflexive-closure_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut lambdaFormation_alt introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality_alt unionEquality applyEquality inhabitedIsType universeIsType hypothesis because_Cache productEquality instantiate independent_pairFormation functionIsType universeEquality inlFormation_alt unionElimination equalitySymmetry equalityTransitivity inrFormation_alt equalityIstype dependent_functionElimination independent_functionElimination rename setElimination dependent_set_memberEquality_alt productElimination dependent_pairEquality_alt inrEquality_alt inlEquality_alt unionIsType productIsType functionEquality isect_memberEquality_alt voidElimination natural_numberEquality

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

Date html generated: 2019_10_15-AM-10_24_56
Last ObjectModification: 2019_08_22-AM-10_51_30

Theory : relations2

Home Index