The positive, negative, and nonnegative rational numbers
Content created by Louis Wasserman and Fredrik Bakke.
Created on 2025-04-25.
Last modified on 2025-10-17.
module elementary-number-theory.positive-and-negative-rational-numbers where
Imports
open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.negative-rational-numbers open import elementary-number-theory.nonnegative-rational-numbers open import elementary-number-theory.nonpositive-rational-numbers open import elementary-number-theory.nonzero-rational-numbers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.function-types open import foundation.functoriality-coproduct-types open import foundation.identity-types open import foundation.negation open import foundation.transport-along-identifications open import foundation.universe-levels
Idea
In this file, we outline basic relations between negative, nonnegative, positive, and nonpositive rational numbers.
Properties
Trichotomies
A rational number is either negative, zero, or positive
abstract trichotomy-sign-ℚ : {l : Level} {A : UU l} (x : ℚ) → ( is-negative-ℚ x → A) → ( x = zero-ℚ → A) → ( is-positive-ℚ x → A) → A trichotomy-sign-ℚ x neg zero pos = trichotomy-le-ℚ ( x) ( zero-ℚ) ( λ x<0 → neg (is-negative-le-zero-ℚ x<0)) ( zero) ( λ 0<x → pos (is-positive-le-zero-ℚ 0<x))
Dichotomies
A rational number is either negative or nonnegative
abstract decide-is-negative-is-nonnegative-ℚ : (q : ℚ) → is-negative-ℚ q + is-nonnegative-ℚ q decide-is-negative-is-nonnegative-ℚ q = map-coproduct ( is-negative-le-zero-ℚ) ( is-nonnegative-leq-zero-ℚ) ( decide-le-leq-ℚ q zero-ℚ)
A rational number is either positive or nonpositive
abstract decide-is-positive-is-nonpositive-ℚ : (q : ℚ) → is-positive-ℚ q + is-nonpositive-ℚ q decide-is-positive-is-nonpositive-ℚ q = map-coproduct ( is-positive-le-zero-ℚ) ( is-nonpositive-leq-zero-ℚ) ( decide-le-leq-ℚ zero-ℚ q)
A rational number is nonpositive or nonnegative
abstract is-nonpositive-or-nonnegative-ℚ : (q : ℚ) → is-nonpositive-ℚ q + is-nonnegative-ℚ q is-nonpositive-or-nonnegative-ℚ q = map-coproduct ( is-nonpositive-leq-zero-ℚ) ( is-nonnegative-leq-zero-ℚ) ( linear-leq-ℚ q zero-ℚ)
If a rational number is nonzero, it is negative or positive
decide-is-negative-is-positive-is-nonzero-ℚ : {q : ℚ} → is-nonzero-ℚ q → is-negative-ℚ q + is-positive-ℚ q decide-is-negative-is-positive-is-nonzero-ℚ {q} q≠0 = trichotomy-sign-ℚ q ( inl) ( ex-falso ∘ q≠0) ( inr)
Implications
Any positive rational number is nonnegative
opaque unfolding is-nonnegative-ℚ is-positive-ℚ is-nonnegative-is-positive-ℚ : {q : ℚ} → is-positive-ℚ q → is-nonnegative-ℚ q is-nonnegative-is-positive-ℚ = is-nonnegative-is-positive-ℤ nonnegative-ℚ⁺ : ℚ⁺ → ℚ⁰⁺ nonnegative-ℚ⁺ (q , H) = (q , is-nonnegative-is-positive-ℚ H)
Any negative rational number is nonpositive
opaque unfolding is-negative-ℚ is-nonpositive-ℚ is-nonpositive-is-negative-ℚ : {q : ℚ} → is-negative-ℚ q → is-nonpositive-ℚ q is-nonpositive-is-negative-ℚ = is-nonnegative-is-positive-ℚ nonpositive-ℚ⁻ : ℚ⁻ → ℚ⁰⁻ nonpositive-ℚ⁻ (q , H) = (q , is-nonpositive-is-negative-ℚ H)
Operations
The negation of a positive rational number is negative
opaque unfolding is-negative-ℚ is-negative-neg-is-positive-ℚ : {q : ℚ} → is-positive-ℚ q → is-negative-ℚ (neg-ℚ q) is-negative-neg-is-positive-ℚ = inv-tr is-positive-ℚ (neg-neg-ℚ _) neg-ℚ⁺ : ℚ⁺ → ℚ⁻ neg-ℚ⁺ (q , is-pos-q) = (neg-ℚ q , is-negative-neg-is-positive-ℚ is-pos-q)
The negation of a negative rational number is positive
opaque unfolding is-negative-ℚ is-positive-neg-is-negative-ℚ : {q : ℚ} → is-negative-ℚ q → is-positive-ℚ (neg-ℚ q) is-positive-neg-is-negative-ℚ = id neg-ℚ⁻ : ℚ⁻ → ℚ⁺ neg-ℚ⁻ (q , is-neg-q) = (neg-ℚ q , is-positive-neg-is-negative-ℚ is-neg-q)
The negation of a nonnegative rational number is nonpositive
opaque unfolding is-nonpositive-ℚ is-nonpositive-neg-is-nonnegative-ℚ : {q : ℚ} → is-nonnegative-ℚ q → is-nonpositive-ℚ (neg-ℚ q) is-nonpositive-neg-is-nonnegative-ℚ = inv-tr is-nonnegative-ℚ (neg-neg-ℚ _) neg-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁻ neg-ℚ⁰⁺ (q , is-nonneg-q) = ( neg-ℚ q , is-nonpositive-neg-is-nonnegative-ℚ is-nonneg-q)
The negation of a nonpositive rational number is nonnegative
opaque unfolding is-nonpositive-ℚ is-nonnegative-neg-is-nonpositive-ℚ : {q : ℚ} → is-nonpositive-ℚ q → is-nonnegative-ℚ (neg-ℚ q) is-nonnegative-neg-is-nonpositive-ℚ = id neg-ℚ⁰⁻ : ℚ⁰⁻ → ℚ⁰⁺ neg-ℚ⁰⁻ (q , is-nonpos-q) = ( neg-ℚ q , is-nonnegative-neg-is-nonpositive-ℚ is-nonpos-q)
Exclusive cases
A rational number is not both negative and positive
abstract is-not-negative-and-positive-ℚ : {x : ℚ} → ¬ (is-negative-ℚ x × is-positive-ℚ x) is-not-negative-and-positive-ℚ {x} (N , P) = not-leq-le-ℚ ( zero-ℚ) ( x) ( le-zero-is-positive-ℚ P) ( leq-zero-is-negative-ℚ N)
A rational number is not both negative and nonnegative
abstract is-not-negative-and-nonnegativeℚ : {x : ℚ} → ¬ (is-negative-ℚ x × is-nonnegative-ℚ x) is-not-negative-and-nonnegativeℚ {x} (N , NN) = not-leq-le-ℚ ( x) ( zero-ℚ) ( le-zero-is-negative-ℚ N) ( leq-zero-is-nonnegative-ℚ NN)
A rational number is not both positive and nonpositive
abstract is-not-positive-and-nonpositive-ℚ : {x : ℚ} → ¬ (is-positive-ℚ x × is-nonpositive-ℚ x) is-not-positive-and-nonpositive-ℚ {x} (P , NP) = not-leq-le-ℚ ( zero-ℚ) ( x) ( le-zero-is-positive-ℚ P) ( leq-zero-is-nonpositive-ℚ NP)
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).