Positive rational numbers
Content created by Louis Wasserman, malarbol, Fredrik Bakke and Garrett Figueroa.
Created on 2024-04-25.
Last modified on 2025-10-17.
{-# OPTIONS --lossy-unification #-} module elementary-number-theory.positive-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.difference-rational-numbers 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.negative-integers open import elementary-number-theory.nonzero-natural-numbers 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.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.decidable-propositions open import foundation.decidable-subtypes open import foundation.dependent-pair-types open import foundation.function-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations 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 set-theory.countable-sets
Idea
A rational number x is said to
be positive¶
if its underlying fraction is
positive.
Positive rational numbers are a subsemigroup of the additive monoid of rational numbers and a submonoid of the multiplicative monoid of rational numbers.
Definitions
The property of being a positive rational number
module _ (x : ℚ) where opaque is-positive-ℚ : UU lzero is-positive-ℚ = is-positive-fraction-ℤ (fraction-ℚ x) is-prop-is-positive-ℚ : is-prop is-positive-ℚ is-prop-is-positive-ℚ = is-prop-is-positive-fraction-ℤ (fraction-ℚ x) is-decidable-prop-is-positive-ℚ : is-decidable-prop is-positive-ℚ is-decidable-prop-is-positive-ℚ = ( is-prop-is-positive-ℚ , is-decidable-is-positive-ℤ (numerator-ℚ x)) is-positive-prop-ℚ : Prop lzero pr1 is-positive-prop-ℚ = is-positive-ℚ pr2 is-positive-prop-ℚ = is-prop-is-positive-ℚ decidable-subtype-positive-ℚ : decidable-subtype lzero ℚ decidable-subtype-positive-ℚ x = ( is-positive-ℚ x , is-decidable-prop-is-positive-ℚ x)
The type of positive rational numbers
positive-ℚ : UU lzero positive-ℚ = type-subtype is-positive-prop-ℚ ℚ⁺ : UU lzero ℚ⁺ = positive-ℚ module _ (x : positive-ℚ) where rational-ℚ⁺ : ℚ rational-ℚ⁺ = pr1 x fraction-ℚ⁺ : fraction-ℤ fraction-ℚ⁺ = fraction-ℚ rational-ℚ⁺ numerator-ℚ⁺ : ℤ numerator-ℚ⁺ = numerator-ℚ rational-ℚ⁺ denominator-ℚ⁺ : ℤ denominator-ℚ⁺ = denominator-ℚ rational-ℚ⁺ is-positive-rational-ℚ⁺ : is-positive-ℚ rational-ℚ⁺ is-positive-rational-ℚ⁺ = pr2 x opaque unfolding is-positive-ℚ is-positive-fraction-ℚ⁺ : is-positive-fraction-ℤ fraction-ℚ⁺ is-positive-fraction-ℚ⁺ = is-positive-rational-ℚ⁺ is-positive-numerator-ℚ⁺ : is-positive-ℤ numerator-ℚ⁺ is-positive-numerator-ℚ⁺ = is-positive-rational-ℚ⁺ 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-positive-prop-ℚ
Properties
The positive rational numbers form a set
set-ℚ⁺ : Set lzero set-ℚ⁺ = set-subset ℚ-Set is-positive-prop-ℚ is-set-ℚ⁺ : is-set ℚ⁺ is-set-ℚ⁺ = is-set-type-Set set-ℚ⁺
The set of positive rational numbers is countable
abstract is-countable-set-ℚ⁺ : is-countable set-ℚ⁺ is-countable-set-ℚ⁺ = is-countable-decidable-subset-is-countable ( ℚ-Set) ( decidable-subtype-positive-ℚ) ( is-countable-ℚ)
The rational image of a positive integer is positive
opaque unfolding is-positive-ℚ is-positive-rational-ℤ : {x : ℤ} → is-positive-ℤ x → is-positive-ℚ (rational-ℤ x) is-positive-rational-ℤ = id positive-rational-positive-ℤ : positive-ℤ → ℚ⁺ positive-rational-positive-ℤ (z , pos-z) = ( rational-ℤ z , is-positive-rational-ℤ pos-z) positive-rational-ℤ⁺ : ℤ⁺ → ℚ⁺ positive-rational-ℤ⁺ = positive-rational-positive-ℤ one-ℚ⁺ : ℚ⁺ one-ℚ⁺ = positive-rational-ℤ⁺ one-ℤ⁺
The type of positive rational numbers is inhabited
abstract is-inhabited-ℚ⁺ : ║ ℚ⁺ ║₋₁ is-inhabited-ℚ⁺ = unit-trunc-Prop one-ℚ⁺
The rational image of a positive natural number is positive
positive-rational-ℕ⁺ : ℕ⁺ → ℚ⁺ positive-rational-ℕ⁺ n = positive-rational-positive-ℤ (positive-int-ℕ⁺ n)
The rational image of a positive integer fraction is positive
opaque unfolding is-positive-ℚ rational-fraction-ℤ is-positive-rational-fraction-ℤ : {x : fraction-ℤ} (P : is-positive-fraction-ℤ x) → is-positive-ℚ (rational-fraction-ℤ x) is-positive-rational-fraction-ℤ = is-positive-reduce-fraction-ℤ
A rational number x is positive if and only if 0 < x
opaque unfolding is-positive-ℚ le-ℚ-Prop le-zero-is-positive-ℚ : {x : ℚ} → is-positive-ℚ x → le-ℚ zero-ℚ x le-zero-is-positive-ℚ {x} = is-positive-eq-ℤ (inv (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))) is-positive-le-zero-ℚ : {x : ℚ} → le-ℚ zero-ℚ x → is-positive-ℚ x is-positive-le-zero-ℚ {x} = is-positive-eq-ℤ (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))
Zero is not a positive rational number
abstract is-not-positive-zero-ℚ : ¬ (is-positive-ℚ zero-ℚ) is-not-positive-zero-ℚ pos-0 = irreflexive-le-ℚ zero-ℚ (le-zero-is-positive-ℚ pos-0)
The difference of a rational number with a lesser rational number is positive
module _ (x y : ℚ) (H : le-ℚ x y) where abstract is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x) is-positive-diff-le-ℚ = is-positive-le-zero-ℚ ( backward-implication ( iff-translate-diff-le-zero-ℚ x y) ( H)) positive-diff-le-ℚ : ℚ⁺ positive-diff-le-ℚ = y -ℚ x , is-positive-diff-le-ℚ left-law-positive-diff-le-ℚ : (rational-ℚ⁺ positive-diff-le-ℚ) +ℚ x = y left-law-positive-diff-le-ℚ = ( associative-add-ℚ y (neg-ℚ x) x) ∙ ( inv-tr ( λ u → y +ℚ u = y) ( left-inverse-law-add-ℚ x) ( right-unit-law-add-ℚ y)) right-law-positive-diff-le-ℚ : x +ℚ (rational-ℚ⁺ positive-diff-le-ℚ) = y right-law-positive-diff-le-ℚ = commutative-add-ℚ x (y -ℚ x) ∙ left-law-positive-diff-le-ℚ
Positive rational numbers are nonzero
opaque unfolding is-positive-ℚ is-nonzero-is-positive-ℚ : {x : ℚ} → is-positive-ℚ x → is-nonzero-ℚ x is-nonzero-is-positive-ℚ {x} H = is-nonzero-is-nonzero-numerator-ℚ x ( is-nonzero-is-positive-ℤ { numerator-ℚ x} ( H)) nonzero-ℚ⁺ : positive-ℚ → nonzero-ℚ nonzero-ℚ⁺ (x , P) = (x , is-nonzero-is-positive-ℚ P)
If p ≤ q and p is positive, then q is positive
abstract is-positive-leq-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → leq-ℚ (rational-ℚ⁺ p) q → is-positive-ℚ q is-positive-leq-ℚ⁺ (p , pos-p) q p≤q = is-positive-le-zero-ℚ ( concatenate-le-leq-ℚ _ _ _ (le-zero-is-positive-ℚ pos-p) p≤q) is-positive-le-ℚ⁺ : (p : ℚ⁺) (q : ℚ) → le-ℚ (rational-ℚ⁺ p) q → is-positive-ℚ q is-positive-le-ℚ⁺ p q p<q = is-positive-leq-ℚ⁺ p q (leq-le-ℚ p<q)
Recent changes
- 2025-10-17. Louis Wasserman. Reorganize signed arithmetic on rational numbers (#1582).
- 2025-10-15. Louis Wasserman. Multiplicative inverses of nonzero real numbers (#1571).
- 2025-10-14. Louis Wasserman. Multiplicative inverses of positive real numbers (#1569).
- 2025-10-11. Louis Wasserman. Square roots of nonnegative real numbers (#1570).
- 2025-10-07. Louis Wasserman. Multiplication of interior intervals in the rational numbers (#1561).