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-07.

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.positive-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.universe-levels

Idea

In this file, we outline basic relations between negative, nonnegative, positive, and nonpositive rational numbers.

Properties

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-ℚ q)
      ( is-nonnegative-leq-zero-ℚ q)
      ( 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-ℚ q)
      ( is-nonpositive-leq-zero-ℚ q)
      ( decide-le-leq-ℚ zero-ℚ q)

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 x<0))
      ( zero)
      ( λ 0<x → pos (is-positive-le-zero-ℚ x 0<x))

Inequalities

A negative rational number is less than a nonnegative rational number

abstract
  le-negative-nonnegative-ℚ :
    (p : ℚ⁻) (q : ℚ⁰⁺) → le-ℚ (rational-ℚ⁻ p) (rational-ℚ⁰⁺ q)
  le-negative-nonnegative-ℚ (p , neg-p) (q , nonneg-q) =
    concatenate-le-leq-ℚ p zero-ℚ q
      ( le-zero-is-negative-ℚ p neg-p)
      ( leq-zero-is-nonnegative-ℚ q nonneg-q)

A nonpositive rational number is less than a positive rational number

abstract
  le-nonpositive-positive-ℚ :
    (p : ℚ⁰⁻) (q : ℚ⁺) → le-ℚ (rational-ℚ⁰⁻ p) (rational-ℚ⁺ q)
  le-nonpositive-positive-ℚ (p , nonpos-p) (q , pos-q) =
    concatenate-leq-le-ℚ p zero-ℚ q
      ( leq-zero-is-nonpositive-ℚ p nonpos-p)
      ( le-zero-is-positive-ℚ q pos-q)

If p < q and p is nonnegative, then q is positive

abstract
  is-positive-le-ℚ⁰⁺ :
    (p : ℚ⁰⁺) (q : ℚ) → le-ℚ (rational-ℚ⁰⁺ p) q → is-positive-ℚ q
  is-positive-le-ℚ⁰⁺ (p , nonneg-p) q p<q =
    is-positive-le-zero-ℚ
      ( q)
      ( concatenate-leq-le-ℚ _ _ _ (leq-zero-is-nonnegative-ℚ p nonneg-p) p<q)

If p < q and q is nonpositive, then p is negative

abstract
  is-negative-le-ℚ⁰⁻ :
    (q : ℚ⁰⁻) (p : ℚ) → le-ℚ p (rational-ℚ⁰⁻ q) → is-negative-ℚ p
  is-negative-le-ℚ⁰⁻ (q , nonpos-q) p p<q =
    is-negative-le-zero-ℚ
      ( p)
      ( concatenate-le-leq-ℚ p q zero-ℚ
        ( p<q)
        ( leq-zero-is-nonpositive-ℚ q nonpos-q))

Recent changes