Nuprl Definition : projective-plane-structure-complete
ProjectivePlaneStructureComplete == ProjectivePlaneStructure"non-trivial":∃p:Point. p ≡ p
Definitions occuring in Statement :
projective-plane-structure: ProjectivePlaneStructure,
pgeo-peq: a ≡ b,
pgeo-point: Point,
exists: ∃x:A. B[x],
token: "$token",
record+: record+
Definitions occuring in definition :
record+: record+,
projective-plane-structure: ProjectivePlaneStructure,
token: "$token",
exists: ∃x:A. B[x],
pgeo-point: Point,
pgeo-peq: a ≡ b
FDL editor aliases :
proj-str-comp
Latex:
ProjectivePlaneStructureComplete == ProjectivePlaneStructure"non-trivial":\mexists{}p:Point. p \mequiv{} p
Date html generated:
2019_10_16-PM-02_11_18
Last ObjectModification:
2018_09_13-PM-04_46_45
Theory : euclidean!plane!geometry
Home
Index