Nonnegative real numbers

Content created by Louis Wasserman and Fredrik Bakke.

Created on 2025-03-26.
Last modified on 2025-10-25.

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

module real-numbers.nonnegative-real-numbers where
Imports 
open import elementary-number-theory.addition-nonnegative-rational-numbers
open import elementary-number-theory.addition-positive-rational-numbers
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-and-negative-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.conjunction
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.existential-quantification
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 metric-spaces.metric-spaces

open import real-numbers.addition-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.difference-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.saturation-inequality-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.strict-inequality-real-numbers
open import real-numbers.subsets-real-numbers

Idea

A real number x is nonnegative if 0 ≤ x.

Definitions

is-nonnegative-ℝ : {l : Level} → ℝ l → UU l
is-nonnegative-ℝ = leq-ℝ zero-ℝ

is-nonnegative-prop-ℝ : {l : Level} → ℝ l → Prop l
is-nonnegative-prop-ℝ = leq-prop-ℝ zero-ℝ

nonnegative-ℝ : (l : Level) → UU (lsuc l)
nonnegative-ℝ l = type-subtype (is-nonnegative-prop-ℝ {l})

ℝ⁰⁺ : (l : Level) → UU (lsuc l)
ℝ⁰⁺ = nonnegative-ℝ

real-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → ℝ l
real-ℝ⁰⁺ = pr1

is-nonnegative-real-ℝ⁰⁺ :
  {l : Level} (x : ℝ⁰⁺ l) → is-nonnegative-ℝ (real-ℝ⁰⁺ x)
is-nonnegative-real-ℝ⁰⁺ = pr2

Properties

Dedekind cuts of nonnegative real numbers

lower-cut-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → subtype l ℚ
lower-cut-ℝ⁰⁺ (x , _) = lower-cut-ℝ x

is-in-lower-cut-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → ℚ → UU l
is-in-lower-cut-ℝ⁰⁺ (x , _) = is-in-lower-cut-ℝ x

is-rounded-lower-cut-ℝ⁰⁺ :
  {l : Level} → (x : ℝ⁰⁺ l) (q : ℚ) →
  (is-in-lower-cut-ℝ⁰⁺ x q ↔ exists ℚ (λ r → le-ℚ-Prop q r ∧ lower-cut-ℝ⁰⁺ x r))
is-rounded-lower-cut-ℝ⁰⁺ (x , _) = is-rounded-lower-cut-ℝ x

upper-cut-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → subtype l ℚ
upper-cut-ℝ⁰⁺ (x , _) = upper-cut-ℝ x

is-in-upper-cut-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → ℚ → UU l
is-in-upper-cut-ℝ⁰⁺ (x , _) = is-in-upper-cut-ℝ x

is-rounded-upper-cut-ℝ⁰⁺ :
  {l : Level} → (x : ℝ⁰⁺ l) (r : ℚ) →
  (is-in-upper-cut-ℝ⁰⁺ x r ↔ exists ℚ (λ q → le-ℚ-Prop q r ∧ upper-cut-ℝ⁰⁺ x q))
is-rounded-upper-cut-ℝ⁰⁺ (x , _) = is-rounded-upper-cut-ℝ x

The nonnegative real numbers form a set

ℝ⁰⁺-Set : (l : Level) → Set (lsuc l)
ℝ⁰⁺-Set l = set-subset (ℝ-Set l) is-nonnegative-prop-ℝ

Equality in the nonnegative real numbers

eq-ℝ⁰⁺ : {l : Level} (x y : ℝ⁰⁺ l) → real-ℝ⁰⁺ x ＝ real-ℝ⁰⁺ y → x ＝ y
eq-ℝ⁰⁺ _ _ = eq-type-subtype is-nonnegative-prop-ℝ

The canonical embedding from nonnegative rational numbers to nonnegative real numbers

abstract
  is-nonnegative-real-ℚ⁰⁺ : (q : ℚ⁰⁺) → is-nonnegative-ℝ (real-ℚ⁰⁺ q)
  is-nonnegative-real-ℚ⁰⁺ (q , nonneg-q) =
    preserves-leq-real-ℚ zero-ℚ q (leq-zero-is-nonnegative-ℚ nonneg-q)

nonnegative-real-ℚ⁰⁺ : ℚ⁰⁺ → ℝ⁰⁺ lzero
nonnegative-real-ℚ⁰⁺ q = (real-ℚ⁰⁺ q , is-nonnegative-real-ℚ⁰⁺ q)

nonnegative-real-ℚ⁺ : ℚ⁺ → ℝ⁰⁺ lzero
nonnegative-real-ℚ⁺ q = nonnegative-real-ℚ⁰⁺ (nonnegative-ℚ⁺ q)

Important nonnegative real numbers

zero-ℝ⁰⁺ : ℝ⁰⁺ lzero
zero-ℝ⁰⁺ = nonnegative-real-ℚ⁰⁺ zero-ℚ⁰⁺

one-ℝ⁰⁺ : ℝ⁰⁺ lzero
one-ℝ⁰⁺ = nonnegative-real-ℚ⁰⁺ one-ℚ⁰⁺

Similarity of nonnegative real numbers

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  sim-prop-ℝ⁰⁺ : Prop (l1 ⊔ l2)
  sim-prop-ℝ⁰⁺ = sim-prop-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y)

  sim-ℝ⁰⁺ : UU (l1 ⊔ l2)
  sim-ℝ⁰⁺ = sim-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y)

infix 6 _~ℝ⁰⁺_
_~ℝ⁰⁺_ : {l1 l2 : Level} → ℝ⁰⁺ l1 → ℝ⁰⁺ l2 → UU (l1 ⊔ l2)
_~ℝ⁰⁺_ = sim-ℝ⁰⁺

sim-zero-prop-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → Prop l
sim-zero-prop-ℝ⁰⁺ = sim-prop-ℝ⁰⁺ zero-ℝ⁰⁺

sim-zero-ℝ⁰⁺ : {l : Level} → ℝ⁰⁺ l → UU l
sim-zero-ℝ⁰⁺ = sim-ℝ⁰⁺ zero-ℝ⁰⁺

eq-sim-ℝ⁰⁺ : {l : Level} (x y : ℝ⁰⁺ l) → sim-ℝ⁰⁺ x y → x ＝ y
eq-sim-ℝ⁰⁺ x y x~y = eq-ℝ⁰⁺ x y (eq-sim-ℝ {x = real-ℝ⁰⁺ x} {y = real-ℝ⁰⁺ y} x~y)

Similarity is symmetric

abstract
  symmetric-sim-ℝ⁰⁺ :
    {l1 l2 : Level} → (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) → x ~ℝ⁰⁺ y → y ~ℝ⁰⁺ x
  symmetric-sim-ℝ⁰⁺ _ _ = symmetric-sim-ℝ

Inequality on nonnegative real numbers

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  leq-prop-ℝ⁰⁺ : Prop (l1 ⊔ l2)
  leq-prop-ℝ⁰⁺ = leq-prop-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y)

  leq-ℝ⁰⁺ : UU (l1 ⊔ l2)
  leq-ℝ⁰⁺ = type-Prop leq-prop-ℝ⁰⁺

Zero is less than or equal to every nonnegative real number

leq-zero-ℝ⁰⁺ : {l : Level} (x : ℝ⁰⁺ l) → leq-ℝ⁰⁺ zero-ℝ⁰⁺ x
leq-zero-ℝ⁰⁺ = is-nonnegative-real-ℝ⁰⁺

Similarity preserves inequality

module _
  {l1 l2 l3 : Level} (z : ℝ⁰⁺ l1) (x : ℝ⁰⁺ l2) (y : ℝ⁰⁺ l3) (x~y : sim-ℝ⁰⁺ x y)
  where

  abstract
    preserves-leq-left-sim-ℝ⁰⁺ : leq-ℝ⁰⁺ x z → leq-ℝ⁰⁺ y z
    preserves-leq-left-sim-ℝ⁰⁺ =
      preserves-leq-left-sim-ℝ (real-ℝ⁰⁺ z) _ _ x~y

Inequality is transitive

module _
  {l1 l2 l3 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) (z : ℝ⁰⁺ l3)
  where

  transitive-leq-ℝ⁰⁺ : leq-ℝ⁰⁺ y z → leq-ℝ⁰⁺ x y → leq-ℝ⁰⁺ x z
  transitive-leq-ℝ⁰⁺ = transitive-leq-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) (real-ℝ⁰⁺ z)

A real number is nonnegative if and only if every element of its upper cut is positive

abstract
  is-positive-is-in-upper-cut-ℝ⁰⁺ :
    {l : Level} → (x : ℝ⁰⁺ l) (q : ℚ) → is-in-upper-cut-ℝ⁰⁺ x q →
    is-positive-ℚ q
  is-positive-is-in-upper-cut-ℝ⁰⁺ (x , 0≤x) q x<q =
    is-positive-le-zero-ℚ
      ( reflects-le-real-ℚ
        ( zero-ℚ)
        ( q)
        ( concatenate-leq-le-ℝ zero-ℝ x _
          ( 0≤x)
          ( le-real-is-in-upper-cut-ℚ q x x<q)))

opaque
  unfolding leq-ℝ leq-ℝ' real-ℚ

  is-nonnegative-is-positive-upper-cut-ℝ :
    {l : Level} → (x : ℝ l) → (upper-cut-ℝ x ⊆ is-positive-prop-ℚ) →
    is-nonnegative-ℝ x
  is-nonnegative-is-positive-upper-cut-ℝ x Uₓ⊆ℚ⁺ =
    leq-leq'-ℝ zero-ℝ x (λ q q∈Uₓ → le-zero-is-positive-ℚ (Uₓ⊆ℚ⁺ q q∈Uₓ))

A real number is nonnegative if and only if every negative rational number is in its lower cut

opaque
  unfolding leq-ℝ real-ℚ

  is-nonnegative-leq-negative-lower-cut-ℝ :
    {l : Level} (x : ℝ l) → (is-negative-prop-ℚ ⊆ lower-cut-ℝ x) →
    is-nonnegative-ℝ x
  is-nonnegative-leq-negative-lower-cut-ℝ x ℚ⁻⊆Lₓ q q<0 =
    ℚ⁻⊆Lₓ q (is-negative-le-zero-ℚ q<0)

  leq-negative-lower-cut-is-nonnegative-ℝ :
    {l : Level} (x : ℝ l) → is-nonnegative-ℝ x →
    (is-negative-prop-ℚ ⊆ lower-cut-ℝ x)
  leq-negative-lower-cut-is-nonnegative-ℝ x 0≤x q is-neg-q =
    0≤x q (le-zero-is-negative-ℚ is-neg-q)

Every nonnegative real number has a positive rational number in its upper cut

abstract
  exists-ℚ⁺-in-upper-cut-ℝ⁰⁺ :
    {l : Level} → (x : ℝ⁰⁺ l) →
    exists ℚ⁺ (λ q → upper-cut-ℝ⁰⁺ x (rational-ℚ⁺ q))
  exists-ℚ⁺-in-upper-cut-ℝ⁰⁺ x =
    let open do-syntax-trunc-Prop (∃ ℚ⁺ (λ q → upper-cut-ℝ⁰⁺ x (rational-ℚ⁺ q)))
    in do
      (q , x<q) ← is-inhabited-upper-cut-ℝ (real-ℝ⁰⁺ x)
      intro-exists (q , is-positive-is-in-upper-cut-ℝ⁰⁺ x q x<q) x<q

Addition on nonnegative real numbers

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  real-add-ℝ⁰⁺ : ℝ (l1 ⊔ l2)
  real-add-ℝ⁰⁺ = real-ℝ⁰⁺ x +ℝ real-ℝ⁰⁺ y

  abstract
    is-nonnegative-real-add-ℝ⁰⁺ : is-nonnegative-ℝ real-add-ℝ⁰⁺
    is-nonnegative-real-add-ℝ⁰⁺ =
      tr
        ( λ z → leq-ℝ z (real-ℝ⁰⁺ x +ℝ real-ℝ⁰⁺ y))
        ( left-unit-law-add-ℝ zero-ℝ)
        ( preserves-leq-add-ℝ
          ( zero-ℝ)
          ( real-ℝ⁰⁺ x)
          ( zero-ℝ)
          ( real-ℝ⁰⁺ y)
          ( is-nonnegative-real-ℝ⁰⁺ x)
          ( is-nonnegative-real-ℝ⁰⁺ y))

  add-ℝ⁰⁺ : ℝ⁰⁺ (l1 ⊔ l2)
  add-ℝ⁰⁺ = (real-add-ℝ⁰⁺ , is-nonnegative-real-add-ℝ⁰⁺)

infixl 35 _+ℝ⁰⁺_

_+ℝ⁰⁺_ : {l1 l2 : Level} → ℝ⁰⁺ l1 → ℝ⁰⁺ l2 → ℝ⁰⁺ (l1 ⊔ l2)
_+ℝ⁰⁺_ = add-ℝ⁰⁺

Unit laws for addition

module _
  {l : Level} (x : ℝ⁰⁺ l)
  where

  abstract
    left-unit-law-add-ℝ⁰⁺ : zero-ℝ⁰⁺ +ℝ⁰⁺ x ＝ x
    left-unit-law-add-ℝ⁰⁺ = eq-ℝ⁰⁺ _ _ (left-unit-law-add-ℝ _)

    right-unit-law-add-ℝ⁰⁺ : x +ℝ⁰⁺ zero-ℝ⁰⁺ ＝ x
    right-unit-law-add-ℝ⁰⁺ = eq-ℝ⁰⁺ _ _ (right-unit-law-add-ℝ _)

Addition preserves inequality

module _
  {l1 l2 l3 l4 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) (z : ℝ⁰⁺ l3) (w : ℝ⁰⁺ l4)
  where

  abstract
    preserves-leq-add-ℝ⁰⁺ :
      leq-ℝ⁰⁺ x y → leq-ℝ⁰⁺ z w → leq-ℝ⁰⁺ (x +ℝ⁰⁺ z) (y +ℝ⁰⁺ w)
    preserves-leq-add-ℝ⁰⁺ =
      preserves-leq-add-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y) (real-ℝ⁰⁺ z) (real-ℝ⁰⁺ w)

If x ≤ y + ε for every ε : ℚ⁺, then x ≤ y

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  abstract
    saturated-leq-ℝ⁰⁺ :
      ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (y +ℝ⁰⁺ nonnegative-real-ℚ⁺ ε)) →
      leq-ℝ⁰⁺ x y
    saturated-leq-ℝ⁰⁺ = saturated-leq-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y)

If a nonnegative real number is less than or equal to all positive rational numbers, it is similar to zero

sim-zero-le-positive-rational-ℝ⁰⁺ :
  {l : Level} (x : ℝ⁰⁺ l) →
  ((ε : ℚ⁺) → leq-ℝ⁰⁺ x (nonnegative-real-ℚ⁺ ε)) →
  sim-zero-ℝ⁰⁺ x
sim-zero-le-positive-rational-ℝ⁰⁺ x H =
  sim-sim-leq-ℝ
    ( leq-zero-ℝ⁰⁺ x ,
      saturated-leq-ℝ⁰⁺
        ( x)
        ( zero-ℝ⁰⁺)
        ( λ ε → inv-tr (leq-ℝ⁰⁺ x) (left-unit-law-add-ℝ⁰⁺ _) (H ε)))

The canonical embedding of nonnegative rational numbers to nonnegative real numbers preserves addition

abstract
  add-nonnegative-real-ℚ⁰⁺ :
    (p q : ℚ⁰⁺) →
    nonnegative-real-ℚ⁰⁺ p +ℝ⁰⁺ nonnegative-real-ℚ⁰⁺ q ＝
    nonnegative-real-ℚ⁰⁺ (p +ℚ⁰⁺ q)
  add-nonnegative-real-ℚ⁰⁺ p q =
    eq-ℝ⁰⁺ _ _ (add-real-ℚ (rational-ℚ⁰⁺ p) (rational-ℚ⁰⁺ q))

The canonical embedding of positive rational numbers to nonnegative real numbers preserves addition

abstract
  add-nonnegative-real-ℚ⁺ :
    (p q : ℚ⁺) →
    nonnegative-real-ℚ⁺ p +ℝ⁰⁺ nonnegative-real-ℚ⁺ q ＝
    nonnegative-real-ℚ⁺ (p +ℚ⁺ q)
  add-nonnegative-real-ℚ⁺ p q =
    eq-ℝ⁰⁺ _ _ (add-real-ℚ (rational-ℚ⁺ p) (rational-ℚ⁺ q))

Nonpositive rational numbers are not less than or equal to nonnegative real numbers

module _
  {l : Level} (x : ℝ⁰⁺ l) (q : ℚ)
  where

  abstract
    not-le-leq-zero-rational-ℝ⁰⁺ :
      leq-ℚ q zero-ℚ → ¬ (le-ℝ (real-ℝ⁰⁺ x) (real-ℚ q))
    not-le-leq-zero-rational-ℝ⁰⁺ q≤0 x<q =
      irreflexive-le-ℝ
        ( real-ℝ⁰⁺ x)
        ( concatenate-le-leq-ℝ _ (real-ℚ q) _
          ( x<q)
          ( transitive-leq-ℝ (real-ℚ q) zero-ℝ (real-ℝ⁰⁺ x)
            ( is-nonnegative-real-ℝ⁰⁺ x)
            ( preserves-leq-real-ℚ _ _ q≤0)))

If a nonnegative real number is less than a rational number, the rational number is positive

module _
  {l : Level} (x : ℝ⁰⁺ l) (q : ℚ)
  where

  abstract
    is-positive-le-nonnegative-real-ℚ :
      le-ℝ (real-ℝ⁰⁺ x) (real-ℚ q) → is-positive-ℚ q
    is-positive-le-nonnegative-real-ℚ x<q =
      is-positive-le-zero-ℚ
        ( reflects-le-real-ℚ _ _
          ( concatenate-leq-le-ℝ _ _ _ (is-nonnegative-real-ℝ⁰⁺ x) x<q))

If x is less than all the positive rational numbers y is less than, then x ≤ y

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  abstract
    leq-le-positive-rational-ℝ⁰⁺ :
      ( (q : ℚ⁺) → le-ℝ (real-ℝ⁰⁺ y) (real-ℚ⁺ q) →
        le-ℝ (real-ℝ⁰⁺ x) (real-ℚ⁺ q)) →
      leq-ℝ⁰⁺ x y
    leq-le-positive-rational-ℝ⁰⁺ H =
      leq-le-rational-ℝ (real-ℝ⁰⁺ x) (real-ℝ⁰⁺ y)
        ( λ q y<q →
          rec-coproduct
            ( λ 0<q →
              let open do-syntax-trunc-Prop (le-prop-ℝ (real-ℝ⁰⁺ x) (real-ℚ q))
              in do
                (p , y<p , p<q) ← dense-rational-le-ℝ _ _ y<q
                transitive-le-ℝ _ (real-ℚ p) _
                  ( p<q)
                  ( H
                    ( p , is-positive-le-nonnegative-real-ℚ y p y<p)
                    ( y<p)))
            ( λ q≤0 → ex-falso (not-le-leq-zero-rational-ℝ⁰⁺ y q q≤0 y<q))
            ( decide-le-leq-ℚ zero-ℚ q))

If x is less than or equal to all the positive rational numbers y is less than or equal to, then x ≤ y

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  abstract
    leq-leq-positive-rational-ℝ⁰⁺ :
      ( (q : ℚ⁺) → leq-ℝ (real-ℝ⁰⁺ y) (real-ℚ⁺ q) →
        leq-ℝ (real-ℝ⁰⁺ x) (real-ℚ⁺ q)) →
      leq-ℝ⁰⁺ x y
    leq-leq-positive-rational-ℝ⁰⁺ H =
      leq-le-positive-rational-ℝ⁰⁺ x y
        ( λ q y<q →
          let open do-syntax-trunc-Prop (le-prop-ℝ _ _)
          in do
            (r , y<r , r<q) ← dense-rational-le-ℝ _ _ y<q
            concatenate-leq-le-ℝ _ _ _
              ( H
                ( r , is-positive-le-nonnegative-real-ℚ y r y<r)
                ( leq-le-ℝ _ _ y<r))
              ( r<q))

If x is less than or equal to the same positive rational numbers y is less than or equal to, then x and y are similar

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  abstract
    sim-leq-same-positive-rational-ℝ⁰⁺ :
      ( (q : ℚ⁺) →
        leq-ℝ (real-ℝ⁰⁺ x) (real-ℚ⁺ q) ↔ leq-ℝ (real-ℝ⁰⁺ y) (real-ℚ⁺ q)) →
      sim-ℝ⁰⁺ x y
    sim-leq-same-positive-rational-ℝ⁰⁺ H =
      sim-sim-leq-ℝ
        ( leq-leq-positive-rational-ℝ⁰⁺ x y (backward-implication ∘ H) ,
          leq-leq-positive-rational-ℝ⁰⁺ y x (forward-implication ∘ H))

If x is less than the same positive rational numbers y is less than, then x and y are similar

module _
  {l1 l2 : Level} (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2)
  where

  abstract
    sim-le-same-positive-rational-ℝ⁰⁺ :
      ( (q : ℚ⁺) →
        le-ℝ (real-ℝ⁰⁺ x) (real-ℚ⁺ q) ↔ le-ℝ (real-ℝ⁰⁺ y) (real-ℚ⁺ q)) →
      sim-ℝ⁰⁺ x y
    sim-le-same-positive-rational-ℝ⁰⁺ H =
      sim-sim-leq-ℝ
        ( leq-le-positive-rational-ℝ⁰⁺ x y (backward-implication ∘ H) ,
          leq-le-positive-rational-ℝ⁰⁺ y x (forward-implication ∘ H))

The metric space of nonnegative real numbers

metric-space-ℝ⁰⁺ : (l : Level) → Metric-Space (lsuc l) l
metric-space-ℝ⁰⁺ l = metric-space-subset-ℝ (is-nonnegative-prop-ℝ {l})

x ≤ y if and only if y - x is nonnegative

module _
  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} (H : leq-ℝ x y)
  where

  abstract
    is-nonnegative-diff-leq-ℝ : is-nonnegative-ℝ (y -ℝ x)
    is-nonnegative-diff-leq-ℝ =
      leq-transpose-left-add-ℝ
        ( zero-ℝ)
        ( x)
        ( y)
        ( inv-tr
          ( λ z → leq-ℝ z y)
          ( left-unit-law-add-ℝ x)
          ( H))

  nonnegative-diff-leq-ℝ : ℝ⁰⁺ (l1 ⊔ l2)
  nonnegative-diff-leq-ℝ = (y -ℝ x , is-nonnegative-diff-leq-ℝ)

abstract
  leq-is-nonnegative-diff-ℝ :
    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → is-nonnegative-ℝ (y -ℝ x) →
    leq-ℝ x y
  leq-is-nonnegative-diff-ℝ x y 0≤y-x =
    tr
      ( λ z → leq-ℝ z y)
      ( left-unit-law-add-ℝ x)
      ( leq-transpose-right-diff-ℝ _ _ _ 0≤y-x)

If a nonnegative real number x is less than or equal to a real number y, y is nonnegative

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

Recent changes