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
- 2025-10-19. Louis Wasserman. Powers of arbitrary rational numbers (#1608).
- 2025-10-09. Louis Wasserman. Multiplication of real numbers (#1384).
- 2025-10-03. Louis Wasserman. Split out operations on nonnegative rational numbers (#1559).