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