Inequality on the positive rational numbers

Content created by Louis Wasserman.

Created on 2025-10-04.
Last modified on 2025-10-04.

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

open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.propositions
open import foundation.universe-levels

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

Idea

The standard ordering on the positive rational numbers is inherited from the standard ordering on rational numbers.

Definition

decidable-total-order-ℚ⁺ : Decidable-Total-Order lzero lzero
decidable-total-order-ℚ⁺ =
  decidable-total-order-Decidable-Total-Suborder
    ℚ-Decidable-Total-Order
    is-positive-prop-ℚ

poset-ℚ⁺ : Poset lzero lzero
poset-ℚ⁺ = poset-Decidable-Total-Order decidable-total-order-ℚ⁺

preorder-ℚ⁺ : Preorder lzero lzero
preorder-ℚ⁺ = preorder-Poset poset-ℚ⁺

leq-prop-ℚ⁺ : ℚ⁺ → ℚ⁺ → Prop lzero
leq-prop-ℚ⁺ = leq-prop-Poset poset-ℚ⁺

leq-ℚ⁺ : ℚ⁺ → ℚ⁺ → UU lzero
leq-ℚ⁺ = leq-Poset poset-ℚ⁺

is-prop-leq-ℚ⁺ : (x y : ℚ⁺) → is-prop (leq-ℚ⁺ x y)
is-prop-leq-ℚ⁺ x y = is-prop-type-Prop (leq-prop-ℚ⁺ x y)

Properties

Inequality on the positive rational numbers is total

is-total-leq-ℚ⁺ : is-total-Poset poset-ℚ⁺
is-total-leq-ℚ⁺ =
  is-total-poset-Decidable-Total-Order decidable-total-order-ℚ⁺

Inequality on the positive rational numbers is decidable

is-decidable-leq-ℚ⁺ : is-decidable-leq-Poset poset-ℚ⁺
is-decidable-leq-ℚ⁺ =
  is-decidable-poset-Decidable-Total-Order decidable-total-order-ℚ⁺

Inequality on the positive rational numbers is a partial order

refl-leq-ℚ⁺ : is-reflexive leq-ℚ⁺
refl-leq-ℚ⁺ = refl-leq-Poset poset-ℚ⁺

transitive-leq-ℚ⁺ : is-transitive leq-ℚ⁺
transitive-leq-ℚ⁺ = transitive-leq-Poset poset-ℚ⁺

antisymmetric-leq-ℚ⁺ : is-antisymmetric leq-ℚ⁺
antisymmetric-leq-ℚ⁺ = antisymmetric-leq-Poset poset-ℚ⁺

Recent changes