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: supposing a euclidean-plane: EuclideanPlane cand: c∧ B sym: Sym(T;x,y.E[x; y]) implies:  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