Saturation of inequality of nonnegative real numbers

Content created by Louis Wasserman.

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

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

module real-numbers.saturation-inequality-nonnegative-real-numbers where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import real-numbers.addition-nonnegative-real-numbers
open import real-numbers.inequality-nonnegative-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.nonnegative-real-numbers
open import real-numbers.saturation-inequality-real-numbers
open import real-numbers.zero-nonnegative-real-numbers

Idea

If x ≤ y + ε for nonnegative real numbers x and y and every positive rational ε, then x ≤ y.

Despite being a property of inequality of nonnegative real numbers, this is much easier to prove via strict inequality, so this page is dedicated to just this property to prevent circular dependency.

Definition

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)

Corollaries

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

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

Recent changes