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