Inequality of nonnegative real numbers

Content created by Louis Wasserman.

Created on 2025-11-09.
Last modified on 2025-11-09.

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

module real-numbers.inequality-nonnegative-real-numbers where
Imports 
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.empty-types
open import foundation.function-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.inequality-real-numbers
open import real-numbers.nonnegative-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-nonnegative-real-numbers
open import real-numbers.strict-inequality-real-numbers

Idea

The standard ordering on the nonnegative real numbers is inherited from the standard ordering on real numbers.

Definition

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-ℝ⁰⁺

Properties

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-ℝ 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)

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))

Recent changes