Nuprl Definition : euclidean-structure
A dependent record type defines the basic types and operations
of Beeson's constructive version of Tarski's geometry.
The first "field" of the record is the type "Point" and the types
of the other fields depend on ⌜self."Point"⌝.
"E" is the congruence relation ⌜ab=cd⌝ and "B" is the strict betweeness
relation ⌜a-b-c⌝. "T" is the non-strict betweeness relation ⌜a_b_c⌝
but it is really a defined concept because the "Tdef" field forces
⌜a_b_c ⇐⇒ ¬((¬(a = b ∈ self."Point")) ∧ (¬(c = b ∈ self."Point")) ∧ (¬a-b-c))⌝.
Simlarly, ⌜Colinear(a;b;c)⌝ is introduced via "colinear" and defined
by "colineardef". These definitions are in the dependent record because
they are needed to give the constrained types for the
"extend", "inner-Pasch", "line-circle" and "middle" operators.
The fields "Estable" and "Bstable" force the congruence and betweeness
propositions to be stable (see Stable{P}, it says ⌜(¬¬P) ⇒ P⌝ ).⋅
EuclideanStructure ==
"Point":Type
"E":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"B":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"T":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"colinear":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
"nontrivial":{trip:self."Point" × self."Point" × self."Point"|
let a,b,c = trip in
(¬(a = b ∈ self."Point")) ∧ (¬(self."colinear" a b c))}
"Tdef":∀[a,b,c:self."Point"].
(self."T" a b c ⇐⇒ ¬((¬(a = b ∈ self."Point")) ∧ (¬(c = b ∈ self."Point")) ∧ (¬(self."B" a b c))))
"colineardef":∀[a,b,c:self."Point"].
(self."colinear" a b c
⇐⇒ (¬(a = b ∈ self."Point"))
∧ (¬((¬(c = a ∈ self."Point"))
∧ (¬(c = b ∈ self."Point"))
∧ (¬(self."B" c a b))
∧ (¬(self."B" a c b))
∧ (¬(self."B" a b c)))))
"Estable":∀[a,b,c,d:self."Point"]. self."E" a b c d supposing ¬¬(self."E" a b c d)
"Bstable":∀[a,b,c:self."Point"]. self."B" a b c supposing ¬¬(self."B" a b c)
"extend":a:self."Point" ⟶ {b:self."Point"| ¬(a = b ∈ self."Point")} ⟶ self."Point" ⟶ self."Point" ⟶ self."Point"
"inner-Pasch":a:self."Point"
⟶ b:self."Point"
⟶ c:{c:self."Point"| ¬(self."colinear" a b c)}
⟶ {p:self."Point"| self."B" a p c}
⟶ {q:self."Point"| self."T" b q c}
⟶ self."Point"
"line-circle":a:self."Point"
⟶ b:self."Point"
⟶ x:{x:self."Point"| self."T" a x b}
⟶ y:{y:self."Point"| self."T" a b y}
⟶ p:{p:self."Point"| self."E" a p a x}
⟶ {q:self."Point"| (self."E" a q a y) ∧ (¬(q = p ∈ self."Point"))}
⟶ (self."Point" × self."Point")
"middle":a:self."Point" ⟶ b:self."Point" ⟶ c:{c:self."Point"| ¬(self."colinear" a b c)} ⟶ self."Point"
Definitions occuring in Statement :
spreadn: spread3,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
top: Top,
prop: ℙ,
iff: P ⇐⇒ Q,
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
token: "$token",
universe: Type,
equal: s = t ∈ T,
record-select: r.x,
record+: record+,
record: record(x.T[x])
Definitions occuring in definition :
apply: f a,
iff: P ⇐⇒ Q,
token: "$token",
record-select: r.x,
uall: ∀[x:A]. B[x],
not: ¬A,
equal: s = t ∈ T,
and: P ∧ Q,
spreadn: spread3,
product: x:A × B[x],
set: {x:A| B[x]} ,
prop: ℙ,
function: x:A ⟶ B[x],
universe: Type,
top: Top,
record: record(x.T[x]),
record+: record+,
uimplies: b supposing a
FDL editor aliases :
eu-struct
Latex:
EuclideanStructure ==
"Point":Type
"E":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} \mBbbP{}
"B":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} \mBbbP{}
"T":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} \mBbbP{}
"colinear":self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} \mBbbP{}
"nontrivial":\{trip:self."Point" \mtimes{} self."Point" \mtimes{} self."Point"|
let a,b,c = trip in
(\mneg{}(a = b)) \mwedge{} (\mneg{}(self."colinear" a b c))\}
"Tdef":\mforall{}[a,b,c:self."Point"].
(self."T" a b c \mLeftarrow{}{}\mRightarrow{} \mneg{}((\mneg{}(a = b)) \mwedge{} (\mneg{}(c = b)) \mwedge{} (\mneg{}(self."B" a b c))))
"colineardef":\mforall{}[a,b,c:self."Point"].
(self."colinear" a b c
\mLeftarrow{}{}\mRightarrow{} (\mneg{}(a = b))
\mwedge{} (\mneg{}((\mneg{}(c = a))
\mwedge{} (\mneg{}(c = b))
\mwedge{} (\mneg{}(self."B" c a b))
\mwedge{} (\mneg{}(self."B" a c b))
\mwedge{} (\mneg{}(self."B" a b c)))))
"Estable":\mforall{}[a,b,c,d:self."Point"]. self."E" a b c d supposing \mneg{}\mneg{}(self."E" a b c d)
"Bstable":\mforall{}[a,b,c:self."Point"]. self."B" a b c supposing \mneg{}\mneg{}(self."B" a b c)
"extend":a:self."Point"
{}\mrightarrow{} \{b:self."Point"| \mneg{}(a = b)\}
{}\mrightarrow{} self."Point"
{}\mrightarrow{} self."Point"
{}\mrightarrow{} self."Point"
"inner-Pasch":a:self."Point"
{}\mrightarrow{} b:self."Point"
{}\mrightarrow{} c:\{c:self."Point"| \mneg{}(self."colinear" a b c)\}
{}\mrightarrow{} \{p:self."Point"| self."B" a p c\}
{}\mrightarrow{} \{q:self."Point"| self."T" b q c\}
{}\mrightarrow{} self."Point"
"line-circle":a:self."Point"
{}\mrightarrow{} b:self."Point"
{}\mrightarrow{} x:\{x:self."Point"| self."T" a x b\}
{}\mrightarrow{} y:\{y:self."Point"| self."T" a b y\}
{}\mrightarrow{} p:\{p:self."Point"| self."E" a p a x\}
{}\mrightarrow{} \{q:self."Point"| (self."E" a q a y) \mwedge{} (\mneg{}(q = p))\}
{}\mrightarrow{} (self."Point" \mtimes{} self."Point")
"middle":a:self."Point"
{}\mrightarrow{} b:self."Point"
{}\mrightarrow{} c:\{c:self."Point"| \mneg{}(self."colinear" a b c)\}
{}\mrightarrow{} self."Point"
Date html generated:
2016_07_08-PM-06_29_42
Last ObjectModification:
2015_09_23-AM-08_59_52
Theory : euclidean!geometry
Home
Index