Nuprl Definition : euclidean-plane-structure
EuclideanPlaneStructure ==
GeometryPrimitives
"Ssquashstable":∀a,b,c,d:Point. SqStable(ab>cd)
"Lorsquashstable":∀a,b,c:Point. SqStable(a leftof bc ∨ a leftof cb)
"SepOr":∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point. (a # c ∨ b # c)
"nontrivial":∃a:Point. (∃b:Point [a # b])
"SS":∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} . (∃x:Point [((¬a # bx) ∧ B(uxv))])
"SC":∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} . (∃u:Point [(cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u))])
"CC":∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:{d:Point| StrictOverlap(a;b;c;d)} .
(∃u:Point [(ab ≅ au ∧ cd ≅ cu ∧ u leftof ac)])
Definitions occuring in Statement :
circle-strict-overlap: StrictOverlap(a;b;c;d),
geo-congruent: ab ≅ cd,
geo-between: B(abc),
geo-lsep: a # bc,
geo-left: a leftof bc,
geo-sep: a # b,
geo-gt-prim: ab>cd,
geo-primitives: GeometryPrimitives,
geo-point: Point,
sq_stable: SqStable(P),
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
token: "$token",
record+: record+
FDL editor aliases :
eu-str
Latex:
EuclideanPlaneStructure ==
GeometryPrimitives
"Ssquashstable":\mforall{}a,b,c,d:Point. SqStable(ab>cd)
"Lorsquashstable":\mforall{}a,b,c:Point. SqStable(a leftof bc \mvee{} a leftof cb)
"SepOr":\mforall{}a:Point. \mforall{}b:\{b:Point| a \# b\} . \mforall{}c:Point. (a \# c \mvee{} b \# c)
"nontrivial":\mexists{}a:Point. (\mexists{}b:Point [a \# b])
"SS":\mforall{}a,b:Point. \mforall{}u:\{u:Point| u leftof ab\} . \mforall{}v:\{v:Point| v leftof ba\} .
(\mexists{}x:Point [((\mneg{}a \# bx) \mwedge{} B(uxv))])
"SC":\mforall{}c,d,a:Point. \mforall{}b:\{b:Point| b \# a \mwedge{} B(cbd)\} .
(\mexists{}u:Point [(cu \mcong{} cd \mwedge{} B(abu) \mwedge{} (b \# d {}\mRightarrow{} b \# u))])
"CC":\mforall{}a,b:Point. \mforall{}c:\{c:Point| a \# c\} . \mforall{}d:\{d:Point| StrictOverlap(a;b;c;d)\} .
(\mexists{}u:Point [(ab \mcong{} au \mwedge{} cd \mcong{} cu \mwedge{} u leftof ac)])
Date html generated:
2020_05_20-AM-09_42_28
Last ObjectModification:
2020_01_29-PM-00_21_26
Theory : euclidean!plane!geometry
Home
Index