### 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