nLab ordered Kock field

Contents

Idea

A definition of ordered field in constructive mathematics which uses denial inequality. It is primarily used in synthetic differential geometry.

Definition

An ordered Kock field is a Kock field RR with a strict weak order <\lt which is not necessarily connected:

  1. for all aRa \in R, ¬(a<a)\neg(a \lt a)

  2. for all aRa \in R and bRb \in R, if a<ba \lt b, then ¬(b<a)\neg(b \lt a)

  3. for all aRa \in R, bRb \in R, and cRc \in R, if a<ca \lt c, then a<ba \lt b or b<cb \lt c

  4. 0<10 \lt 1

  5. for all aRa \in R and bRb \in R, if 0<a0 \lt a and 0<b0 \lt b, then 0<a+b0 \lt a + b

  6. for all aRa \in R and bRb \in R, if 0<a0 \lt a and 0<b0 \lt b, then 0<ab0 \lt a \cdot b

  7. for all aRa \in R, a0a \neq 0 if and only if a<0a \lt 0 or 0<a0 \lt a

 See also

References

Last revised on March 2, 2024 at 15:54:38. See the history of this page for a list of all contributions to it.