### Nuprl Lemma : eu-seg-congruent-equiv

`∀e:EuclideanPlane. EquivRel(Segment;s,t.s ≡ t)`

Proof

Definitions occuring in Statement :  eu-seg-congruent: `s1 ≡ s2` eu-segment: `Segment` euclidean-plane: `EuclideanPlane` equiv_rel: `EquivRel(T;x,y.E[x; y])` all: `∀x:A. B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])` member: `t ∈ T` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` euclidean-plane: `EuclideanPlane` cand: `A c∧ B` sym: `Sym(T;x,y.E[x; y])` implies: `P `` Q` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])`
Lemmas referenced :  eu-seg-congruent_weakening eu-segment_wf eu-seg-congruent_symmetry eu-seg-congruent_wf euclidean-plane_wf eu-seg-congruent_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache isectElimination independent_isectElimination hypothesis setElimination rename hypothesisEquality

Latex:
\mforall{}e:EuclideanPlane.  EquivRel(Segment;s,t.s  \mequiv{}  t)

Date html generated: 2016_05_18-AM-06_36_52
Last ObjectModification: 2015_12_28-AM-09_25_40

Theory : euclidean!geometry

Home Index