Nuprl Definition : projective-plane
ProjectivePlane ==
{g:ProjectivePlaneStructureComplete| BasicProjectiveGeometryAxioms(g) ∧ triangle-axiom1(g) ∧ triangle-axiom2(g)}
Definitions occuring in Statement :
triangle-axiom2: triangle-axiom2(g),
triangle-axiom1: triangle-axiom1(g),
projective-plane-structure-complete: ProjectivePlaneStructureComplete,
basic-pgeo-axioms: BasicProjectiveGeometryAxioms(g),
and: P ∧ Q,
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
projective-plane-structure-complete: ProjectivePlaneStructureComplete,
basic-pgeo-axioms: BasicProjectiveGeometryAxioms(g),
and: P ∧ Q,
triangle-axiom1: triangle-axiom1(g),
triangle-axiom2: triangle-axiom2(g)
FDL editor aliases :
proj-pl
Latex:
ProjectivePlane ==
\{g:ProjectivePlaneStructureComplete|
BasicProjectiveGeometryAxioms(g) \mwedge{} triangle-axiom1(g) \mwedge{} triangle-axiom2(g)\}
Date html generated:
2018_05_22-PM-00_40_45
Last ObjectModification:
2017_11_26-PM-07_53_16
Theory : euclidean!plane!geometry
Home
Index