Nuprl Definition : projective-plane-structure
ProjectivePlaneStructure ==
  ProjGeomPrimitives
  "Ssquashstable":∀l:Line. ∀a:Point.  SqStable(a ≠ l)
  "PLSepOr":∀a:Point. ∀l:{l:Line| a ≠ l} . ∀m:Line.  (a ≠ m ∨ m ≠ l)
  "LPSepOr":∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Point.  (b ≠ l ∨ b ≠ a)
  "join":∀a,b:Point.  (a ≠ b 
⇒ (∃l:Line. (a I l ∧ b I l)))
  "meet":∀l,m:Line.  (l ≠ m 
⇒ (∃a:Point. (a I l ∧ a I m)))
  "three-points":∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a)
  "three-lines":∀a:Point. ∃l,m,n:Line. (a I l ∧ a I m ∧ a I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)
Definitions occuring in Statement : 
pgeo-lpsep: a ≠ b
, 
pgeo-lsep: l ≠ m
, 
pgeo-psep: a ≠ b
, 
pgeo-incident: a I b
, 
pgeo-plsep: a ≠ b
, 
pgeo-primitives: ProjGeomPrimitives
, 
pgeo-line: Line
, 
pgeo-point: Point
, 
sq_stable: SqStable(P)
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
token: "$token"
, 
record+: record+
Definitions occuring in definition : 
and: P ∧ Q
, 
pgeo-lsep: l ≠ m
, 
pgeo-incident: a I b
, 
pgeo-line: Line
, 
exists: ∃x:A. B[x]
, 
pgeo-point: Point
, 
all: ∀x:A. B[x]
, 
token: "$token"
, 
pgeo-psep: a ≠ b
, 
implies: P 
⇒ Q
, 
pgeo-plsep: a ≠ b
, 
or: P ∨ Q
, 
pgeo-lpsep: a ≠ b
, 
set: {x:A| B[x]} 
, 
sq_stable: SqStable(P)
, 
pgeo-primitives: ProjGeomPrimitives
, 
record+: record+
FDL editor aliases : 
proj-str
Latex:
ProjectivePlaneStructure  ==
    ProjGeomPrimitives
    "Ssquashstable":\mforall{}l:Line.  \mforall{}a:Point.    SqStable(a  \mneq{}  l)
    "PLSepOr":\mforall{}a:Point.  \mforall{}l:\{l:Line|  a  \mneq{}  l\}  .  \mforall{}m:Line.    (a  \mneq{}  m  \mvee{}  m  \mneq{}  l)
    "LPSepOr":\mforall{}l:Line.  \mforall{}a:\{a:Point|  l  \mneq{}  a\}  .  \mforall{}b:Point.    (b  \mneq{}  l  \mvee{}  b  \mneq{}  a)
    "join":\mforall{}a,b:Point.    (a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}l:Line.  (a  I  l  \mwedge{}  b  I  l)))
    "meet":\mforall{}l,m:Line.    (l  \mneq{}  m  {}\mRightarrow{}  (\mexists{}a:Point.  (a  I  l  \mwedge{}  a  I  m)))
    "three-points":\mforall{}l:Line.  \mexists{}a,b,c:Point.  (a  I  l  \mwedge{}  b  I  l  \mwedge{}  c  I  l  \mwedge{}  a  \mneq{}  b  \mwedge{}  b  \mneq{}  c  \mwedge{}  c  \mneq{}  a)
    "three-lines":\mforall{}a:Point.  \mexists{}l,m,n:Line.  (a  I  l  \mwedge{}  a  I  m  \mwedge{}  a  I  n  \mwedge{}  l  \mneq{}  m  \mwedge{}  m  \mneq{}  n  \mwedge{}  n  \mneq{}  l)
Date html generated:
2018_05_22-PM-00_26_38
Last ObjectModification:
2017_11_26-PM-01_42_06
Theory : euclidean!plane!geometry
Home
Index