The positive, negative, and nonnegative rational numbers

Content created by Louis Wasserman.

Created on 2025-04-25.
Last modified on 2025-04-25.

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.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.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.universe-levels

Idea

In this file, we outline basic relations between negative, nonnegative, and positive 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-ℚ)

Trichotomies

A rational number is either negative, zero, or positive

abstract
  trichotomy-sign-ℚ :
    {l : Level} {A : UU l} (x : ℚ) →
    ( is-negative-ℚ x → A) →
    ( Id 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))

Recent changes