Nuprl Definition : euclidean-plane
Beeson's axioms for constructive geometry.
The EuclideanStructure includes the basic types and
four operations with constructive content.
The four basic constructions are
1) extending a segment, 
2) intersecting lines,
3) intersecting a line and a circle, 
4) circumscribing a triangle. 
The euclidean-axioms(e)
are constraints on the euclidean structures that have no constructive
content -- they assert the congruence and betweeness properties of the
four basic constructions.
⋅
EuclideanPlane ==  {e:EuclideanStructure| euclidean-axioms(e)} 
Definitions occuring in Statement : 
euclidean-axioms: euclidean-axioms(e)
, 
euclidean-structure: EuclideanStructure
, 
set: {x:A| B[x]} 
Definitions occuring in definition : 
set: {x:A| B[x]} 
, 
euclidean-structure: EuclideanStructure
, 
euclidean-axioms: euclidean-axioms(e)
FDL editor aliases : 
eu-pl
Latex:
EuclideanPlane  ==    \{e:EuclideanStructure|  euclidean-axioms(e)\} 
Date html generated:
2016_07_08-PM-06_29_47
Last ObjectModification:
2015_09_23-AM-09_00_03
Theory : euclidean!geometry
Home
Index