Decidable total orders
Content created by Louis Wasserman, Fredrik Bakke, Egbert Rijke, Julian KG, fernabnor, louismntnu and malarbol.
Created on 2023-05-05.
Last modified on 2025-10-02.
module order-theory.decidable-total-orders where
Imports
open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.coproduct-types open import foundation.decidable-propositions open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels open import order-theory.decidable-posets open import order-theory.decidable-total-preorders open import order-theory.greatest-lower-bounds-posets open import order-theory.join-semilattices open import order-theory.least-upper-bounds-posets open import order-theory.meet-semilattices open import order-theory.posets open import order-theory.preorders open import order-theory.subposets open import order-theory.total-orders
Idea
A decidable total order is a total order of which the inequality relation is decidable.
Definitions
The predicate on posets of being decidable total orders
is-decidable-total-prop-Poset : {l1 l2 : Level} → Poset l1 l2 → Prop (l1 ⊔ l2) is-decidable-total-prop-Poset P = product-Prop (is-total-Poset-Prop P) (is-decidable-leq-prop-Poset P) is-decidable-total-Poset : {l1 l2 : Level} → Poset l1 l2 → UU (l1 ⊔ l2) is-decidable-total-Poset P = type-Prop (is-decidable-total-prop-Poset P) is-prop-is-decidable-total-Poset : {l1 l2 : Level} (P : Poset l1 l2) → is-prop (is-decidable-total-Poset P) is-prop-is-decidable-total-Poset P = is-prop-type-Prop (is-decidable-total-prop-Poset P)
The type of decidable total orders
Decidable-Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Decidable-Total-Order l1 l2 = Σ (Poset l1 l2) (is-decidable-total-Poset) module _ {l1 l2 : Level} (P : Decidable-Total-Order l1 l2) where poset-Decidable-Total-Order : Poset l1 l2 poset-Decidable-Total-Order = pr1 P is-total-poset-Decidable-Total-Order : is-total-Poset (poset-Decidable-Total-Order) is-total-poset-Decidable-Total-Order = pr1 (pr2 P) total-order-Decidable-Total-Order : Total-Order l1 l2 total-order-Decidable-Total-Order = ( poset-Decidable-Total-Order , is-total-poset-Decidable-Total-Order) is-decidable-poset-Decidable-Total-Order : is-decidable-leq-Poset (poset-Decidable-Total-Order) is-decidable-poset-Decidable-Total-Order = pr2 (pr2 P) type-Decidable-Total-Order : UU l1 type-Decidable-Total-Order = type-Poset poset-Decidable-Total-Order leq-Decidable-Total-Order-Prop : (x y : type-Decidable-Total-Order) → Prop l2 leq-Decidable-Total-Order-Prop = leq-prop-Poset poset-Decidable-Total-Order leq-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → UU l2 leq-Decidable-Total-Order = leq-Poset poset-Decidable-Total-Order is-prop-leq-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → is-prop (leq-Decidable-Total-Order x y) is-prop-leq-Decidable-Total-Order = is-prop-leq-Poset poset-Decidable-Total-Order le-Decidable-Total-Order-Prop : (x y : type-Decidable-Total-Order) → Prop (l1 ⊔ l2) le-Decidable-Total-Order-Prop = le-prop-Poset poset-Decidable-Total-Order le-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → UU (l1 ⊔ l2) le-Decidable-Total-Order = le-Poset poset-Decidable-Total-Order is-prop-le-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → is-prop (le-Decidable-Total-Order x y) is-prop-le-Decidable-Total-Order = is-prop-le-Poset poset-Decidable-Total-Order decidable-poset-Decidable-Total-Order : Decidable-Poset l1 l2 pr1 decidable-poset-Decidable-Total-Order = poset-Decidable-Total-Order pr2 decidable-poset-Decidable-Total-Order = is-decidable-poset-Decidable-Total-Order leq-total-decidable-poset-decidable-Prop : (x y : type-Decidable-Total-Order) → Decidable-Prop l2 leq-total-decidable-poset-decidable-Prop = leq-decidable-poset-decidable-Prop decidable-poset-Decidable-Total-Order concatenate-eq-leq-Decidable-Total-Order : {x y z : type-Decidable-Total-Order} → x = y → leq-Decidable-Total-Order y z → leq-Decidable-Total-Order x z concatenate-eq-leq-Decidable-Total-Order = concatenate-eq-leq-Poset poset-Decidable-Total-Order concatenate-leq-eq-Decidable-Total-Order : {x y z : type-Decidable-Total-Order} → leq-Decidable-Total-Order x y → y = z → leq-Decidable-Total-Order x z concatenate-leq-eq-Decidable-Total-Order = concatenate-leq-eq-Poset poset-Decidable-Total-Order refl-leq-Decidable-Total-Order : is-reflexive leq-Decidable-Total-Order refl-leq-Decidable-Total-Order = refl-leq-Poset poset-Decidable-Total-Order transitive-leq-Decidable-Total-Order : is-transitive leq-Decidable-Total-Order transitive-leq-Decidable-Total-Order = transitive-leq-Poset poset-Decidable-Total-Order preorder-Decidable-Total-Order : Preorder l1 l2 preorder-Decidable-Total-Order = preorder-Poset poset-Decidable-Total-Order decidable-total-preorder-Decidable-Total-Order : Decidable-Total-Preorder l1 l2 pr1 decidable-total-preorder-Decidable-Total-Order = preorder-Decidable-Total-Order pr1 (pr2 decidable-total-preorder-Decidable-Total-Order) = is-total-poset-Decidable-Total-Order pr2 (pr2 decidable-total-preorder-Decidable-Total-Order) = is-decidable-poset-Decidable-Total-Order leq-or-strict-greater-Decidable-Poset : (x y : type-Decidable-Total-Order) → UU (l1 ⊔ l2) leq-or-strict-greater-Decidable-Poset = leq-or-strict-greater-Decidable-Preorder decidable-total-preorder-Decidable-Total-Order is-leq-or-strict-greater-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → leq-or-strict-greater-Decidable-Poset x y is-leq-or-strict-greater-Decidable-Total-Order = is-leq-or-strict-greater-Decidable-Total-Preorder decidable-total-preorder-Decidable-Total-Order antisymmetric-leq-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → leq-Decidable-Total-Order x y → leq-Decidable-Total-Order y x → Id x y antisymmetric-leq-Decidable-Total-Order = antisymmetric-leq-Poset poset-Decidable-Total-Order is-prop-leq-or-strict-greater-Decidable-Total-Order : (x y : type-Decidable-Total-Order) → is-prop (leq-or-strict-greater-Decidable-Poset x y) is-prop-leq-or-strict-greater-Decidable-Total-Order x y = is-prop-coproduct ( λ p q → pr1 q (inv (antisymmetric-leq-Decidable-Total-Order x y p (pr2 q)))) ( is-prop-leq-Decidable-Total-Order x y) ( is-prop-le-Decidable-Total-Order y x) is-set-type-Decidable-Total-Order : is-set type-Decidable-Total-Order is-set-type-Decidable-Total-Order = is-set-type-Poset poset-Decidable-Total-Order set-Decidable-Total-Order : Set l1 set-Decidable-Total-Order = set-Poset poset-Decidable-Total-Order
Properties
Any two elements in a decidable total order have a minimum and maximum
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where min-Decidable-Total-Order : type-Decidable-Total-Order T → type-Decidable-Total-Order T → type-Decidable-Total-Order T min-Decidable-Total-Order = min-Total-Order (total-order-Decidable-Total-Order T) max-Decidable-Total-Order : type-Decidable-Total-Order T → type-Decidable-Total-Order T → type-Decidable-Total-Order T max-Decidable-Total-Order = max-Total-Order (total-order-Decidable-Total-Order T)
The binary minimum is the binary greatest lower bound
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) (x y : type-Decidable-Total-Order T) where min-is-greatest-binary-lower-bound-Decidable-Total-Order : is-greatest-binary-lower-bound-Poset ( poset-Decidable-Total-Order T) ( x) ( y) ( min-Decidable-Total-Order T x y) min-is-greatest-binary-lower-bound-Decidable-Total-Order = min-is-greatest-binary-lower-bound-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y) has-greatest-binary-lower-bound-Decidable-Total-Order : has-greatest-binary-lower-bound-Poset (poset-Decidable-Total-Order T) x y has-greatest-binary-lower-bound-Decidable-Total-Order = has-greatest-binary-lower-bound-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y)
The minimum of two values is a lower bound
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) (x y : type-Decidable-Total-Order T) where leq-left-min-Decidable-Total-Order : leq-Decidable-Total-Order T (min-Decidable-Total-Order T x y) x leq-left-min-Decidable-Total-Order = leq-left-min-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y) leq-right-min-Decidable-Total-Order : leq-Decidable-Total-Order T (min-Decidable-Total-Order T x y) y leq-right-min-Decidable-Total-Order = leq-right-min-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y)
The maximum of two values is their least upper bound
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) (x y : type-Decidable-Total-Order T) where max-is-least-binary-upper-bound-Decidable-Total-Order : is-least-binary-upper-bound-Poset ( poset-Decidable-Total-Order T) ( x) ( y) ( max-Decidable-Total-Order T x y) max-is-least-binary-upper-bound-Decidable-Total-Order = max-is-least-binary-upper-bound-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y) has-least-binary-upper-bound-Decidable-Total-Order : has-least-binary-upper-bound-Poset (poset-Decidable-Total-Order T) x y pr1 has-least-binary-upper-bound-Decidable-Total-Order = max-Decidable-Total-Order T x y pr2 has-least-binary-upper-bound-Decidable-Total-Order = max-is-least-binary-upper-bound-Decidable-Total-Order
The maximum of two values is an upper bound
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) (x y : type-Decidable-Total-Order T) where leq-left-max-Decidable-Total-Order : leq-Decidable-Total-Order T x (max-Decidable-Total-Order T x y) leq-left-max-Decidable-Total-Order = leq-left-max-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y) leq-right-max-Decidable-Total-Order : leq-Decidable-Total-Order T y (max-Decidable-Total-Order T x y) leq-right-max-Decidable-Total-Order = leq-right-max-Total-Order ( total-order-Decidable-Total-Order T) ( x) ( y)
The minimum of two values is less than or equal to their maximum
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) (x y : type-Decidable-Total-Order T) where abstract min-leq-max-Decidable-Total-Order : leq-Decidable-Total-Order T ( min-Decidable-Total-Order T x y) ( max-Decidable-Total-Order T x y) min-leq-max-Decidable-Total-Order = min-leq-max-Total-Order (total-order-Decidable-Total-Order T) x y
Decidable total orders are meet semilattices
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where is-meet-semilattice-Decidable-Total-Order : is-meet-semilattice-Poset (poset-Decidable-Total-Order T) is-meet-semilattice-Decidable-Total-Order = is-meet-semilattice-Total-Order ( total-order-Decidable-Total-Order T) order-theoretic-meet-semilattice-Decidable-Total-Order : Order-Theoretic-Meet-Semilattice l1 l2 order-theoretic-meet-semilattice-Decidable-Total-Order = order-theoretic-meet-semilattice-Total-Order ( total-order-Decidable-Total-Order T)
Decidable total orders are join semilattices
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where is-join-semilattice-Decidable-Total-Order : is-join-semilattice-Poset (poset-Decidable-Total-Order T) is-join-semilattice-Decidable-Total-Order = is-join-semilattice-Total-Order ( total-order-Decidable-Total-Order T) order-theoretic-join-semilattice-Decidable-Total-Order : Order-Theoretic-Join-Semilattice l1 l2 order-theoretic-join-semilattice-Decidable-Total-Order = order-theoretic-join-semilattice-Total-Order ( total-order-Decidable-Total-Order T)
The binary minimum operation is associative
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where associative-min-Decidable-Total-Order : (x y z : type-Decidable-Total-Order T) → min-Decidable-Total-Order T (min-Decidable-Total-Order T x y) z = min-Decidable-Total-Order T x (min-Decidable-Total-Order T y z) associative-min-Decidable-Total-Order = associative-min-Total-Order ( total-order-Decidable-Total-Order T)
The binary maximum operation is associative
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where associative-max-Decidable-Total-Order : (x y z : type-Decidable-Total-Order T) → max-Decidable-Total-Order T (max-Decidable-Total-Order T x y) z = max-Decidable-Total-Order T x (max-Decidable-Total-Order T y z) associative-max-Decidable-Total-Order = associative-max-Total-Order ( total-order-Decidable-Total-Order T)
The binary minimum operation is commutative
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where commutative-min-Decidable-Total-Order : (x y : type-Decidable-Total-Order T) → min-Decidable-Total-Order T x y = min-Decidable-Total-Order T y x commutative-min-Decidable-Total-Order = commutative-min-Total-Order ( total-order-Decidable-Total-Order T)
The binary maximum operation is commutative
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where commutative-max-Decidable-Total-Order : (x y : type-Decidable-Total-Order T) → max-Decidable-Total-Order T x y = max-Decidable-Total-Order T y x commutative-max-Decidable-Total-Order = commutative-max-Total-Order ( total-order-Decidable-Total-Order T)
The binary minimum operation is idempotent
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where idempotent-min-Decidable-Total-Order : (x : type-Decidable-Total-Order T) → min-Decidable-Total-Order T x x = x idempotent-min-Decidable-Total-Order = idempotent-min-Total-Order ( total-order-Decidable-Total-Order T)
The binary maximum operation is idempotent
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where idempotent-max-Decidable-Total-Order : (x : type-Decidable-Total-Order T) → max-Decidable-Total-Order T x x = x idempotent-max-Decidable-Total-Order = idempotent-max-Total-Order ( total-order-Decidable-Total-Order T)
If x
is less than or equal to y
, the minimum of x
and y
is x
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where left-leq-right-min-Decidable-Total-Order : (x y : type-Decidable-Total-Order T) → leq-Decidable-Total-Order T x y → min-Decidable-Total-Order T x y = x left-leq-right-min-Decidable-Total-Order = left-leq-right-min-Total-Order (total-order-Decidable-Total-Order T)
If y
is less than or equal to x
, the minimum of x
and y
is y
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where right-leq-left-min-Decidable-Total-Order : (x y : type-Decidable-Total-Order T) → leq-Decidable-Total-Order T y x → min-Decidable-Total-Order T x y = y right-leq-left-min-Decidable-Total-Order = right-leq-left-min-Total-Order (total-order-Decidable-Total-Order T)
If x
is less than or equal to y
, the maximum of x
and y
is y
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where left-leq-right-max-Decidable-Total-Order : (x y : type-Decidable-Total-Order T) → leq-Decidable-Total-Order T x y → max-Decidable-Total-Order T x y = y left-leq-right-max-Decidable-Total-Order = left-leq-right-max-Total-Order (total-order-Decidable-Total-Order T)
If y
is less than or equal to x
, the maximum of x
and y
is x
module _ {l1 l2 : Level} (T : Decidable-Total-Order l1 l2) where right-leq-left-max-Decidable-Total-Order : (x y : type-Decidable-Total-Order T) → leq-Decidable-Total-Order T y x → max-Decidable-Total-Order T x y = x right-leq-left-max-Decidable-Total-Order = right-leq-left-max-Total-Order (total-order-Decidable-Total-Order T)
If a ≤ b
and c ≤ d
, then min a c ≤ min b d
min-leq-leq-Decidable-Total-Order : (a b c d : type-Decidable-Total-Order T) → leq-Decidable-Total-Order T a b → leq-Decidable-Total-Order T c d → leq-Decidable-Total-Order ( T) ( min-Decidable-Total-Order T a c) ( min-Decidable-Total-Order T b d) min-leq-leq-Decidable-Total-Order = min-leq-leq-Total-Order ( total-order-Decidable-Total-Order T)
If a ≤ b
and c ≤ d
, then max a c ≤ max b d
max-leq-leq-Decidable-Total-Order : (a b c d : type-Decidable-Total-Order T) → leq-Decidable-Total-Order T a b → leq-Decidable-Total-Order T c d → leq-Decidable-Total-Order ( T) ( max-Decidable-Total-Order T a c) ( max-Decidable-Total-Order T b d) max-leq-leq-Decidable-Total-Order = max-leq-leq-Total-Order ( total-order-Decidable-Total-Order T)
Subsets of decidable total orders are decidable total orders
Decidable-Total-Suborder : {l1 l2 : Level} (l3 : Level) → Decidable-Total-Order l1 l2 → UU (l1 ⊔ lsuc l3) Decidable-Total-Suborder l3 T = Subposet l3 (poset-Decidable-Total-Order T) module _ {l1 l2 l3 : Level} (T : Decidable-Total-Order l1 l2) (P : Decidable-Total-Suborder l3 T) where is-total-leq-Decidable-Total-Suborder : is-total-Poset (poset-Subposet (poset-Decidable-Total-Order T) P) is-total-leq-Decidable-Total-Suborder x y = is-total-poset-Decidable-Total-Order ( T) ( inclusion-subtype P x) ( inclusion-subtype P y) is-decidable-leq-Decidable-Total-Suborder : is-decidable-leq-Poset (poset-Subposet (poset-Decidable-Total-Order T) P) is-decidable-leq-Decidable-Total-Suborder x y = is-decidable-poset-Decidable-Total-Order ( T) ( inclusion-subtype P x) ( inclusion-subtype P y) decidable-total-order-Decidable-Total-Suborder : Decidable-Total-Order (l1 ⊔ l3) l2 decidable-total-order-Decidable-Total-Suborder = poset-Subposet (poset-Decidable-Total-Order T) P , is-total-leq-Decidable-Total-Suborder , is-decidable-leq-Decidable-Total-Suborder
Recent changes
- 2025-10-02. Louis Wasserman. Intervals and interval arithmetic (#1497).
- 2025-08-30. Louis Wasserman. Minimum and maximum for total orders (#1490).
- 2025-04-24. malarbol. Bernoulli’s inequality on the positive rational numbers (#1371).
- 2025-03-24. Louis Wasserman. Minimum and maximum on the lower, upper, and usual Dedekind real numbers (#1335).
- 2025-02-13. Louis Wasserman. Minimum and maximum are associative (#1300).