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 segment, 
2) intersecting lines,
3) intersecting line and circle, 
4) circumscribing 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

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