Showing changes from revision #10 to #11:
Added | Removed | Changed
Contents
Definition
Abelian Propositions groups
An A abelian proposition group is a pointed type set with a an binary identification operation called for all elementssubtraction such and that.
-
for all ,
-
for all ,
-
for all and ,
-
for all , , and ,
Sets
Halving groups
A set is a type such that for all elements and , the identity type is a proposition.
A halving group is an abelian group G with a function called halving or dividing by two such that for all , .
Pointed abelian groups
Totally ordered halving groups
A pointed abelian group is a set with an element called one and a binary operation called subtraction such that
An abelian group is a totally ordered abelian group if it comes with a function such that
-
for all elements ,
-
for all elements ,
-
for all elements and ,
-
for all elements , , and ,
-
for all elements ,
-
for all elements and ,
-
for all elements , , and ,
-
for all elements and , implies that for all elements ,
-
for all elements and , or
Pointed halving groups
A pointed halving group is a pointed abelian group G with a function called halving or dividing by two such that for all elements , .
Totally ordered pointed halving groups
A pointed halving group is a totally ordered pointed halving group if it comes with a function such that
-
for all elements ,
-
for all elements and ,
-
for all elements , , and ,
-
for all elements and , or
-
for all elements and , implies that for all elements ,
Strictly ordered pointed halving groups
A totally ordered commutative pointed ring halving group is a strictly ordered pointed abelian group if it comes with an a element type family and a type family such that
- for all elements and , is a proposition
- for all elements , is false
- for all elements , , and , if , then or
- for all elements and , if is false and is false, then
- for all elements and , if , then is false.
- for all elements and , if and , then
… The initial strictly ordered pointed halving group is the dyadic rational numbers.
Archimedean ordered pointed halving groups
A strictly ordered pointed halving group is an Archimedean ordered pointed halving group if for all elements and , if , then there merely exists a dyadic rational number such that and .
Sequentially Cauchy complete Archimedean ordered pointed halving groups
Let be an Archimedean ordered pointed halving group and let
be the positive elements in . is sequentially Cauchy complete if every Cauchy sequence in converges:
A sequence in is a function .
A sequence is a Cauchy sequence if for all positive elements , there merely exists a natural number such that for all natural numbers and such that and , .
An element is said to be a limit of the sequence if for all positive elements , there merely exists a natural number such that for all natural numbers such that ,
is sequentially Cauchy complete if every Cauchy sequence in merely has a limit.