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