Nuprl Lemma : sq_stable_eu-seg-congruent
∀e:EuclideanStructure. ∀[s1,s2:Segment]. SqStable(s1 ≡ s2)
Proof
Definitions occuring in Statement :
eu-seg-congruent: s1 ≡ s2,
eu-segment: Segment,
euclidean-structure: EuclideanStructure,
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
eu-seg-congruent: s1 ≡ s2,
member: t ∈ T
Lemmas referenced :
sq_stable__eu-congruent,
eu-seg1_wf,
eu-seg2_wf,
eu-segment_wf,
euclidean-structure_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
hypothesis
Latex:
\mforall{}e:EuclideanStructure. \mforall{}[s1,s2:Segment]. SqStable(s1 \mequiv{} s2)
Date html generated:
2016_05_18-AM-06_36_42
Last ObjectModification:
2015_12_28-AM-09_25_35
Theory : euclidean!geometry
Home
Index