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