Strict inequality on nonnegative rational numbers
Content created by Louis Wasserman.
Created on 2025-10-03.
Last modified on 2025-10-19.
module elementary-number-theory.strict-inequality-nonnegative-rational-numbers where
Imports
open import elementary-number-theory.inequality-nonnegative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.dependent-pair-types open import foundation.propositions open import foundation.universe-levels
Idea
The standard strict ordering¶ on the nonnegative rational numbers is inherited from the standard strict ordering on rational numbers.
Definition
le-prop-ℚ⁰⁺ : (p q : ℚ⁰⁺) → Prop lzero le-prop-ℚ⁰⁺ p q = le-ℚ-Prop (rational-ℚ⁰⁺ p) (rational-ℚ⁰⁺ q) le-ℚ⁰⁺ : (p q : ℚ⁰⁺) → UU lzero le-ℚ⁰⁺ p q = type-Prop (le-prop-ℚ⁰⁺ p q)
Properties
Strict inequality on the nonnegative rational numbers is transitive
abstract transitive-le-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → le-ℚ⁰⁺ q r → le-ℚ⁰⁺ p q → le-ℚ⁰⁺ p r transitive-le-ℚ⁰⁺ (p , _) (q , _) (r , _) = transitive-le-ℚ p q r
Concatenation laws with inequality
abstract concatenate-le-leq-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → le-ℚ⁰⁺ p q → leq-ℚ⁰⁺ q r → le-ℚ⁰⁺ p r concatenate-le-leq-ℚ⁰⁺ (p , _) (q , _) (r , _) = concatenate-le-leq-ℚ p q r concatenate-leq-le-ℚ⁰⁺ : (p q r : ℚ⁰⁺) → leq-ℚ⁰⁺ p q → le-ℚ⁰⁺ q r → le-ℚ⁰⁺ p r concatenate-leq-le-ℚ⁰⁺ (p , _) (q , _) (r , _) = concatenate-leq-le-ℚ p q r
Recent changes
- 2025-10-19. Louis Wasserman. Powers of arbitrary rational numbers (#1608).
- 2025-10-17. Louis Wasserman. Reorganize signed arithmetic on rational numbers (#1582).
- 2025-10-03. Louis Wasserman. Split out operations on nonnegative rational numbers (#1559).