Inequality on the nonnegative rational numbers

Content created by Louis Wasserman.

Created on 2025-10-03.
Last modified on 2025-10-19.

module elementary-number-theory.inequality-nonnegative-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.nonnegative-rational-numbers

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

open import order-theory.decidable-total-orders

Idea

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

Definition

leq-prop-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → Prop lzero
leq-prop-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ-Prop p q

leq-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → UU lzero
leq-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ p q

Properties

The decidable total order of nonnegative rational numbers

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

Inequality on the nonnegative rational numbers is transitive

abstract
  transitive-leq-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → leq-ℚ⁰⁺ q r → leq-ℚ⁰⁺ p q → leq-ℚ⁰⁺ p r
  transitive-leq-ℚ⁰⁺ (p , _) (q , _) (r , _) = transitive-leq-ℚ p q r

Recent changes