Positive and negative real numbers

Content created by Louis Wasserman.

Created on 2025-10-15.
Last modified on 2026-01-14.

{-# OPTIONS --lossy-unification #-}

module real-numbers.positive-and-negative-real-numbers where
Imports 
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.negative-real-numbers
open import real-numbers.nonnegative-real-numbers
open import real-numbers.nonpositive-real-numbers
open import real-numbers.positive-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.strict-inequality-real-numbers

Idea

On this page, we outline basic relations between negative, nonnegative, and positive real numbers.

Properties

Positive real numbers are nonnegative

abstract
  is-nonnegative-is-positive-ℝ :
    {l : Level} {x : ℝ l} → is-positive-ℝ x → is-nonnegative-ℝ x
  is-nonnegative-is-positive-ℝ = leq-le-ℝ

nonnegative-ℝ⁺ : {l : Level} → ℝ⁺ l → ℝ⁰⁺ l
nonnegative-ℝ⁺ (x , is-pos-x) = (x , is-nonnegative-is-positive-ℝ is-pos-x)

The negation of a positive real number is negative

abstract
  neg-is-positive-ℝ :
    {l : Level} (x : ℝ l) → is-positive-ℝ x → is-negative-ℝ (neg-ℝ x)
  neg-is-positive-ℝ x 0<x =
    tr
      ( le-ℝ (neg-ℝ x))
      ( neg-zero-ℝ)
      ( neg-le-ℝ 0<x)

neg-ℝ⁺ : {l : Level} → ℝ⁺ l → ℝ⁻ l
neg-ℝ⁺ (x , is-pos-x) = (neg-ℝ x , neg-is-positive-ℝ x is-pos-x)

The negation of a negative real number is positive

abstract
  neg-is-negative-ℝ :
    {l : Level} (x : ℝ l) → is-negative-ℝ x → is-positive-ℝ (neg-ℝ x)
  neg-is-negative-ℝ x x<0 =
    tr
      ( λ z → le-ℝ z (neg-ℝ x))
      ( neg-zero-ℝ)
      ( neg-le-ℝ x<0)

neg-ℝ⁻ : {l : Level} → ℝ⁻ l → ℝ⁺ l
neg-ℝ⁻ (x , is-neg-x) = (neg-ℝ x , neg-is-negative-ℝ x is-neg-x)

The negation of a nonnegative real number is nonpositive

abstract
  neg-is-nonnegative-ℝ :
    {l : Level} (x : ℝ l) → is-nonnegative-ℝ x → is-nonpositive-ℝ (neg-ℝ x)
  neg-is-nonnegative-ℝ x 0≤x =
    tr
      ( leq-ℝ (neg-ℝ x))
      ( neg-zero-ℝ)
      ( neg-leq-ℝ 0≤x)

neg-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → ℝ⁰⁻ l
neg-ℝ⁰⁺ (x , 0≤x) = (neg-ℝ x , neg-is-nonnegative-ℝ x 0≤x)

The negation of a nonpositive real number is nonnegative

abstract
  neg-is-nonpositive-ℝ :
    {l : Level} (x : ℝ l) → is-nonpositive-ℝ x → is-nonnegative-ℝ (neg-ℝ x)
  neg-is-nonpositive-ℝ x x≤0 =
    tr
      ( λ z → leq-ℝ z (neg-ℝ x))
      ( neg-zero-ℝ)
      ( neg-leq-ℝ x≤0)

neg-ℝ⁰⁻ : {l : Level} → ℝ⁰⁻ l → ℝ⁰⁺ l
neg-ℝ⁰⁻ (x , x≤0) = (neg-ℝ x , neg-is-nonpositive-ℝ x x≤0)

A real number is negative if and only if its negation is positive

abstract
  is-negative-is-positive-neg-ℝ :
    {l : Level} (x : ℝ l) → is-positive-ℝ (neg-ℝ x) → is-negative-ℝ x
  is-negative-is-positive-neg-ℝ x 0<-x =
    tr is-negative-ℝ (neg-neg-ℝ x) (neg-is-positive-ℝ (neg-ℝ x) 0<-x)

is-negative-iff-neg-is-positive-ℝ :
  {l : Level} (x : ℝ l) → is-negative-ℝ x ↔ is-positive-ℝ (neg-ℝ x)
is-negative-iff-neg-is-positive-ℝ x =
  ( neg-is-negative-ℝ x ,
    is-negative-is-positive-neg-ℝ x)

A real number is positive if and only if its negation is negative

abstract
  is-positive-is-negative-neg-ℝ :
    {l : Level} (x : ℝ l) → is-negative-ℝ (neg-ℝ x) → is-positive-ℝ x
  is-positive-is-negative-neg-ℝ x -x<0 =
    tr is-positive-ℝ (neg-neg-ℝ x) (neg-is-negative-ℝ (neg-ℝ x) -x<0)

is-positive-iff-neg-is-negative-ℝ :
  {l : Level} (x : ℝ l) → is-positive-ℝ x ↔ is-negative-ℝ (neg-ℝ x)
is-positive-iff-neg-is-negative-ℝ x =
  ( neg-is-positive-ℝ x ,
    is-positive-is-negative-neg-ℝ x)

A real number is nonpositive if and only if its negation is nonnegative

abstract
  is-nonpositive-is-nonnegative-neg-ℝ :
    {l : Level} (x : ℝ l) → is-nonnegative-ℝ (neg-ℝ x) → is-nonpositive-ℝ x
  is-nonpositive-is-nonnegative-neg-ℝ x 0≤-x =
    tr is-nonpositive-ℝ (neg-neg-ℝ x) (neg-is-nonnegative-ℝ (neg-ℝ x) 0≤-x)

If a nonnegative real number x is less than a real number y, y is positive

abstract
  is-positive-le-ℝ⁰⁺ :
    {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ l2) → le-ℝ (real-ℝ⁰⁺ x) y →
    is-positive-ℝ y
  is-positive-le-ℝ⁰⁺ (x , 0≤x) y = concatenate-leq-le-ℝ zero-ℝ x y 0≤x

Real numbers are not both negative and nonnegative

abstract
  is-not-negative-and-nonnegative-ℝ :
    {l : Level} {x : ℝ l} → ¬ (is-negative-ℝ x × is-nonnegative-ℝ x)
  is-not-negative-and-nonnegative-ℝ {x = x} (x<0 , 0≤x) =
    not-leq-le-ℝ x zero-ℝ x<0 0≤x

Real numbers are not both negative and positive

abstract
  is-not-negative-and-positive-ℝ :
    {l : Level} {x : ℝ l} → ¬ (is-negative-ℝ x × is-positive-ℝ x)
  is-not-negative-and-positive-ℝ (x<0 , 0<x) = asymmetric-le-ℝ x<0 0<x

Recent changes