Nonnegative rational numbers
Content created by Louis Wasserman.
Created on 2025-04-01.
Last modified on 2025-04-01.
{-# OPTIONS --lossy-unification #-} module elementary-number-theory.nonnegative-rational-numbers where
Imports
open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.cross-multiplication-difference-integer-fractions open import elementary-number-theory.decidable-total-order-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-integers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integer-fractions open import elementary-number-theory.integers open import elementary-number-theory.multiplication-integer-fractions open import elementary-number-theory.multiplication-integers open import elementary-number-theory.multiplication-positive-and-negative-integers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.nonnegative-integer-fractions open import elementary-number-theory.nonnegative-integers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integer-fractions open import elementary-number-theory.positive-integers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.reduced-integer-fractions open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels open import order-theory.inflationary-maps-posets
Idea
A rational number x
is said to
be
nonnegative¶
if its numerator is a
nonnegative integer.
Nonnegative rational numbers are a subsemigroup of the additive monoid of rational numbers.
Definitions
The property of being a nonnegative rational number
module _ (q : ℚ) where is-nonnegative-ℚ : UU lzero is-nonnegative-ℚ = is-nonnegative-fraction-ℤ (fraction-ℚ q) is-prop-is-nonnegative-ℚ : is-prop is-nonnegative-ℚ is-prop-is-nonnegative-ℚ = is-prop-is-nonnegative-fraction-ℤ (fraction-ℚ q) is-nonnegative-prop-ℚ : Prop lzero pr1 is-nonnegative-prop-ℚ = is-nonnegative-ℚ pr2 is-nonnegative-prop-ℚ = is-prop-is-nonnegative-ℚ
The type of nonnegative rational numbers
nonnegative-ℚ : UU lzero nonnegative-ℚ = type-subtype is-nonnegative-prop-ℚ ℚ⁰⁺ : UU lzero ℚ⁰⁺ = nonnegative-ℚ module _ (x : nonnegative-ℚ) where rational-ℚ⁰⁺ : ℚ rational-ℚ⁰⁺ = pr1 x fraction-ℚ⁰⁺ : fraction-ℤ fraction-ℚ⁰⁺ = fraction-ℚ rational-ℚ⁰⁺ numerator-ℚ⁰⁺ : ℤ numerator-ℚ⁰⁺ = numerator-ℚ rational-ℚ⁰⁺ denominator-ℚ⁰⁺ : ℤ denominator-ℚ⁰⁺ = denominator-ℚ rational-ℚ⁰⁺ is-nonnegative-rational-ℚ⁰⁺ : is-nonnegative-ℚ rational-ℚ⁰⁺ is-nonnegative-rational-ℚ⁰⁺ = pr2 x is-nonnegative-fraction-ℚ⁰⁺ : is-nonnegative-fraction-ℤ fraction-ℚ⁰⁺ is-nonnegative-fraction-ℚ⁰⁺ = pr2 x is-nonnegative-numerator-ℚ⁰⁺ : is-nonnegative-ℤ numerator-ℚ⁰⁺ is-nonnegative-numerator-ℚ⁰⁺ = is-nonnegative-fraction-ℚ⁰⁺ is-positive-denominator-ℚ⁰⁺ : is-positive-ℤ denominator-ℚ⁰⁺ is-positive-denominator-ℚ⁰⁺ = is-positive-denominator-ℚ rational-ℚ⁰⁺ abstract eq-ℚ⁰⁺ : {x y : ℚ⁰⁺} → rational-ℚ⁰⁺ x = rational-ℚ⁰⁺ y → x = y eq-ℚ⁰⁺ {x} {y} = eq-type-subtype is-nonnegative-prop-ℚ zero-ℚ⁰⁺ : ℚ⁰⁺ zero-ℚ⁰⁺ = zero-ℚ , _
Properties
The nonnegative rational numbers form a set
is-set-ℚ⁰⁺ : is-set ℚ⁰⁺ is-set-ℚ⁰⁺ = is-set-type-subtype is-nonnegative-prop-ℚ is-set-ℚ
The rational image of a nonnegative integer is nonnegative
abstract is-nonnegative-rational-ℤ : (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℚ (rational-ℤ x) is-nonnegative-rational-ℤ _ H = H nonnegative-rational-nonnegative-ℤ : nonnegative-ℤ → ℚ⁰⁺ nonnegative-rational-nonnegative-ℤ (x , x-is-neg) = ( rational-ℤ x , is-nonnegative-rational-ℤ x x-is-neg)
The rational image of a nonnegative integer fraction is nonnegative
abstract is-nonnegative-rational-fraction-ℤ : {x : fraction-ℤ} (P : is-nonnegative-fraction-ℤ x) → is-nonnegative-ℚ (rational-fraction-ℤ x) is-nonnegative-rational-fraction-ℤ {x} = is-nonnegative-sim-fraction-ℤ ( x) ( reduce-fraction-ℤ x) ( sim-reduced-fraction-ℤ x)
A rational number x
is nonnegative if and only if 0 ≤ x
module _ (x : ℚ) where abstract leq-zero-is-nonnegative-ℚ : is-nonnegative-ℚ x → leq-ℚ zero-ℚ x leq-zero-is-nonnegative-ℚ = is-nonnegative-eq-ℤ (inv (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))) is-nonnegative-leq-zero-ℚ : leq-ℚ zero-ℚ x → is-nonnegative-ℚ x is-nonnegative-leq-zero-ℚ = is-nonnegative-eq-ℤ (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x)) is-nonnegative-iff-leq-zero-ℚ : is-nonnegative-ℚ x ↔ leq-ℚ zero-ℚ x is-nonnegative-iff-leq-zero-ℚ = ( leq-zero-is-nonnegative-ℚ , is-nonnegative-leq-zero-ℚ)
The difference of a rational number with a rational number less than or equal to the first is nonnegative
module _ (x y : ℚ) (H : leq-ℚ x y) where abstract is-nonnegative-diff-leq-ℚ : is-nonnegative-ℚ (y -ℚ x) is-nonnegative-diff-leq-ℚ = is-nonnegative-leq-zero-ℚ ( y -ℚ x) ( backward-implication (iff-translate-diff-leq-zero-ℚ x y) H) nonnegative-diff-le-ℚ : ℚ⁰⁺ nonnegative-diff-le-ℚ = (y -ℚ x , is-nonnegative-diff-leq-ℚ)
The product of two nonnegative rational numbers is nonnegative
is-nonnegative-mul-nonnegative-ℚ : {x y : ℚ} → is-nonnegative-ℚ x → is-nonnegative-ℚ y → is-nonnegative-ℚ (x *ℚ y) is-nonnegative-mul-nonnegative-ℚ {x} {y} P Q = is-nonnegative-rational-fraction-ℤ ( is-nonnegative-mul-nonnegative-fraction-ℤ { fraction-ℚ x} { fraction-ℚ y} ( P) ( Q))
Multiplication by a nonnegative rational number preserves inequality
abstract preserves-leq-right-mul-ℚ⁰⁺ : (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r → leq-ℚ (q *ℚ rational-ℚ⁰⁺ p) (r *ℚ rational-ℚ⁰⁺ p) preserves-leq-right-mul-ℚ⁰⁺ p⁺@((p@(np , dp , pos-dp) , _) , nonneg-np) (q@(nq , dq , _) , _) (r@(nr , dr , _) , _) q≤r = preserves-leq-rational-fraction-ℤ ( mul-fraction-ℤ q p) ( mul-fraction-ℤ r p) ( binary-tr ( leq-ℤ) ( interchange-law-mul-mul-ℤ _ _ _ _) ( interchange-law-mul-mul-ℤ _ _ _ _) ( preserves-leq-left-mul-nonnegative-ℤ ( np *ℤ dp , is-nonnegative-mul-nonnegative-positive-ℤ nonneg-np pos-dp) ( nq *ℤ dr) ( nr *ℤ dq) ( q≤r))) preserves-leq-left-mul-ℚ⁰⁺ : (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r → leq-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r) preserves-leq-left-mul-ℚ⁰⁺ p q r q≤r = binary-tr ( leq-ℚ) ( commutative-mul-ℚ q (rational-ℚ⁰⁺ p)) ( commutative-mul-ℚ r (rational-ℚ⁰⁺ p)) ( preserves-leq-right-mul-ℚ⁰⁺ p q r q≤r)
Addition on nonnegative rational numbers
abstract is-nonnegative-add-ℚ : (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q → is-nonnegative-ℚ (p +ℚ q) is-nonnegative-add-ℚ p q nonneg-p nonneg-q = is-nonnegative-rational-fraction-ℤ ( is-nonnegative-add-fraction-ℤ { fraction-ℚ p} { fraction-ℚ q} ( nonneg-p) ( nonneg-q)) add-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ add-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) = ( p +ℚ q , is-nonnegative-add-ℚ p q nonneg-p nonneg-q) infixl 35 _+ℚ⁰⁺_ _+ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ _+ℚ⁰⁺_ = add-ℚ⁰⁺
Multiplication on nonnegative rational numbers
abstract is-nonnegative-mul-ℚ : (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q → is-nonnegative-ℚ (p *ℚ q) is-nonnegative-mul-ℚ p q nonneg-p nonneg-q = is-nonnegative-rational-fraction-ℤ ( is-nonnegative-mul-nonnegative-fraction-ℤ { fraction-ℚ p} { fraction-ℚ q} ( nonneg-p) ( nonneg-q)) mul-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ mul-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) = ( p *ℚ q , is-nonnegative-mul-ℚ p q nonneg-p nonneg-q) infixl 35 _*ℚ⁰⁺_ _*ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺ _*ℚ⁰⁺_ = mul-ℚ⁰⁺
Inequality on nonnegative rational numbers
leq-ℚ⁰⁺-Prop : ℚ⁰⁺ → ℚ⁰⁺ → Prop lzero leq-ℚ⁰⁺-Prop (p , _) (q , _) = leq-ℚ-Prop p q leq-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → UU lzero leq-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ p q
Addition of a nonnegative rational number is an increasing map
abstract is-inflationary-map-left-add-rational-ℚ⁰⁺ : (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (rational-ℚ⁰⁺ p +ℚ_) is-inflationary-map-left-add-rational-ℚ⁰⁺ (p , nonneg-p) q = tr ( λ r → leq-ℚ r (p +ℚ q)) ( left-unit-law-add-ℚ q) ( preserves-leq-left-add-ℚ ( q) ( zero-ℚ) ( p) ( leq-zero-is-nonnegative-ℚ p nonneg-p)) is-inflationary-map-right-add-rational-ℚ⁰⁺ : (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (_+ℚ rational-ℚ⁰⁺ p) is-inflationary-map-right-add-rational-ℚ⁰⁺ p q = tr ( leq-ℚ q) ( commutative-add-ℚ (rational-ℚ⁰⁺ p) q) ( is-inflationary-map-left-add-rational-ℚ⁰⁺ p q)
Recent changes
- 2025-04-01. Louis Wasserman. Absolute value on rational numbers (#1381).