The decidable total order of rational numbers

Content created by Fredrik Bakke and malarbol.

Created on 2024-03-28.
Last modified on 2024-03-28.

module elementary-number-theory.decidable-total-order-rational-numbers where
Imports 
open import elementary-number-theory.inequality-rational-numbers

open import foundation.dependent-pair-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import order-theory.decidable-total-orders
open import order-theory.total-orders

Idea

The type of rational numbers equipped with its standard ordering relation forms a decidable total order.

Definition

is-total-leq-ℚ : is-total-Poset ℚ-Poset
is-total-leq-ℚ x y = unit-trunc-Prop (linear-leq-ℚ x y)

ℚ-Total-Order : Total-Order lzero lzero
pr1 ℚ-Total-Order = ℚ-Poset
pr2 ℚ-Total-Order = is-total-leq-ℚ

ℚ-Decidable-Total-Order : Decidable-Total-Order lzero lzero
pr1 ℚ-Decidable-Total-Order = ℚ-Poset
pr1 (pr2 ℚ-Decidable-Total-Order) = is-total-leq-ℚ
pr2 (pr2 ℚ-Decidable-Total-Order) = is-decidable-leq-ℚ

Recent changes