Nuprl Lemma : Euclid-Prop9-ext
∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| c # ba} . ∃f:Point. acf ≅a bcf
Proof
Definitions occuring in Statement :
geo-cong-angle: abc ≅a xyz,
euclidean-plane: EuclideanPlane,
geo-lsep: a # bc,
geo-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
set: {x:A| B[x]}
Definitions unfolded in proof :
member: t ∈ T,
record-select: r.x,
Euclid-Prop9,
geo-extend-exists,
sq_stable__geo-lsep,
Euclid-Prop10,
geo-sep-sym,
sq_stable__geo-sep,
geo-between-trivial,
geo-congruent-iff-length,
geo-congruent-refl,
Euclid-midpoint,
sq_stable__and,
sq_stable__geo-between,
sq_stable__geo-congruent,
basic-geo-sep-sym,
sq_stable__geo-axioms,
sq_stable__geo-gt-prim,
geo-seg-congruent-iff-length,
geo-cong-preserves-gt-prim,
sq_stable-geo-axioms-if,
any: any x,
stable-implies-sq_stable,
stable__geo-between,
sq_stable__all
Latex:
\mforall{}e:EuclideanPlane. \mforall{}a,b:Point. \mforall{}c:\{c:Point| c \# ba\} . \mexists{}f:Point. acf \mcong{}\msuba{} bcf
Date html generated:
2020_05_20-AM-10_03_18
Last ObjectModification:
2020_01_27-PM-07_13_36
Theory : euclidean!plane!geometry
Home
Index