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