### Nuprl Lemma : meq_inversion

[X:Type]. ∀[d:metric(X)]. ∀[x,y:X].  y ≡ supposing x ≡ y

Proof

Definitions occuring in Statement :  meq: x ≡ y metric: metric(X) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a meq: x ≡ y metric: metric(X) implies:  Q prop: guard: {T} equiv_rel: EquivRel(T;x,y.E[x; y]) and: P ∧ Q sym: Sym(T;x,y.E[x; y]) all: x:A. B[x]
Lemmas referenced :  meq-equiv req_witness int-to-real_wf meq_wf metric_wf istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule applyEquality setElimination rename natural_numberEquality independent_functionElimination universeIsType isect_memberEquality_alt because_Cache isectIsTypeImplies inhabitedIsType instantiate universeEquality productElimination dependent_functionElimination

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[x,y:X].    y  \mequiv{}  x  supposing  x  \mequiv{}  y

Date html generated: 2019_10_29-AM-10_55_36
Last ObjectModification: 2019_10_02-AM-09_36_54

Theory : reals

Home Index