An abelian group is a totally ordered abelian group if it comes with a function such that
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
Strictly ordered pointed abelian groups
A totally ordered commutative ring is a strictly ordered pointed abelian group if it comes with an element 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
Strictly ordered pointed -vector space
…
Archimedean ordered pointed -vector space
A strictly ordered pointed -vector space is an Archimedean ordered pointed -vector space if for all elements and , if , then there merely exists a rational number such that and .
Sequentially Cauchy complete Archimedean ordered pointed -vector space
Let be an Archimedean ordered pointed -vector space and let
be the positive elements in . is sequentially Cauchy complete if every Cauchy sequence in converges: