Nuprl Lemma : eu-seg-congruent_weakening
∀e:EuclideanPlane. ∀[s1,s2:Segment]. s1 ≡ s2 supposing s1 = s2 ∈ Segment
Proof
Definitions occuring in Statement :
eu-seg-congruent: s1 ≡ s2,
eu-segment: Segment,
euclidean-plane: EuclideanPlane,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
eu-seg-congruent: s1 ≡ s2,
euclidean-plane: EuclideanPlane,
prop: ℙ
Lemmas referenced :
eu-congruent-refl,
eu-seg1_wf,
eu-seg2_wf,
eu-congruent_wf,
equal_wf,
eu-segment_wf,
euclidean-plane_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
introduction,
axiomEquality,
hypothesis,
thin,
rename,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
hypothesisEquality,
isectElimination,
setElimination,
because_Cache,
hyp_replacement,
equalitySymmetry,
Error :applyLambdaEquality,
sqequalRule
Latex:
\mforall{}e:EuclideanPlane. \mforall{}[s1,s2:Segment]. s1 \mequiv{} s2 supposing s1 = s2
Date html generated:
2016_10_26-AM-07_41_28
Last ObjectModification:
2016_07_12-AM-08_07_34
Theory : euclidean!geometry
Home
Index