Nuprl Definition : basic-pgeo-axioms
BasicProjectiveGeometryAxioms(g) ==
∀m,l:Line. ∀p,q:Point. (p I l ⇒ q I l ⇒ p I m ⇒ q I m ⇒ (¬((¬p ≡ q) ∧ (¬l ≡ m))))
Definitions occuring in Statement :
pgeo-leq: a ≡ b,
pgeo-peq: a ≡ b,
pgeo-incident: a I b,
pgeo-line: Line,
pgeo-point: Point,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
pgeo-line: Line,
all: ∀x:A. B[x],
pgeo-point: Point,
implies: P ⇒ Q,
pgeo-incident: a I b,
and: P ∧ Q,
pgeo-peq: a ≡ b,
not: ¬A,
pgeo-leq: a ≡ b
FDL editor aliases :
basic-pgeo-axioms
Latex:
BasicProjectiveGeometryAxioms(g) ==
\mforall{}m,l:Line. \mforall{}p,q:Point. (p I l {}\mRightarrow{} q I l {}\mRightarrow{} p I m {}\mRightarrow{} q I m {}\mRightarrow{} (\mneg{}((\mneg{}p \mequiv{} q) \mwedge{} (\mneg{}l \mequiv{} m))))
Date html generated:
2019_10_16-PM-02_11_03
Last ObjectModification:
2018_08_02-PM-00_30_26
Theory : euclidean!plane!geometry
Home
Index