Nuprl Definition : Playfair-axiom
Playfair-axiom(e) == ∀p:Point. ∀l,m,n:Line. ((p I m ∧ m || l) ⇒ (p I n ∧ n || l) ⇒ m ≡ n)
Definitions occuring in Statement :
geo-Aparallel: l || m,
geo-incident: p I L,
geo-line-eq: l ≡ m,
geo-line: Line,
geo-point: Point,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions occuring in definition :
geo-line-eq: l ≡ m,
geo-Aparallel: l || m,
geo-incident: p I L,
and: P ∧ Q,
implies: P ⇒ Q,
geo-line: Line,
all: ∀x:A. B[x],
geo-point: Point
FDL editor aliases :
Playfair-axiom
Latex:
Playfair-axiom(e) == \mforall{}p:Point. \mforall{}l,m,n:Line. ((p I m \mwedge{} m || l) {}\mRightarrow{} (p I n \mwedge{} n || l) {}\mRightarrow{} m \mequiv{} n)
Date html generated:
2018_05_22-PM-01_08_09
Last ObjectModification:
2018_05_11-PM-10_46_55
Theory : euclidean!plane!geometry
Home
Index