The binary minimum of real numbers

Content created by Louis Wasserman.

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

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

module real-numbers.binary-minimum-real-numbers where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.binary-transport
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import order-theory.greatest-lower-bounds-large-posets
open import order-theory.large-meet-semilattices
open import order-theory.meet-semilattices

open import real-numbers.addition-real-numbers
open import real-numbers.binary-maximum-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.negation-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.strict-inequality-real-numbers

Idea

The minimum of two Dedekind real numbers x and y is their greatest lower bound.

Definition

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

  opaque
    min-ℝ : ℝ (l1 ⊔ l2)
    min-ℝ = neg-ℝ (max-ℝ (neg-ℝ x) (neg-ℝ y))

Properties

The binary minimum is a greatest lower bound

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

  opaque
    unfolding leq-ℝ min-ℝ

    is-greatest-binary-lower-bound-min-ℝ :
      is-greatest-binary-lower-bound-Large-Poset
        ( ℝ-Large-Poset)
        ( x)
        ( y)
        ( min-ℝ x y)
    pr1 (is-greatest-binary-lower-bound-min-ℝ z) (z≤x , z≤y) =
      tr
        ( λ w → leq-ℝ w (min-ℝ x y))
        ( neg-neg-ℝ z)
        ( neg-leq-ℝ (max-ℝ (neg-ℝ x) (neg-ℝ y)) (neg-ℝ z)
          ( leq-max-leq-leq-ℝ _ _ (neg-ℝ z)
            ( neg-leq-ℝ z x z≤x)
            ( neg-leq-ℝ z y z≤y)))
    pr2 (is-greatest-binary-lower-bound-min-ℝ z) z≤min =
      let
        case :
          {l : Level} (w : ℝ l) → leq-ℝ (neg-ℝ w) (max-ℝ (neg-ℝ x) (neg-ℝ y)) →
          leq-ℝ z w
        case w -w≤max =
          transitive-leq-ℝ z (min-ℝ x y) w
            ( tr
              ( leq-ℝ (min-ℝ x y))
              ( neg-neg-ℝ _)
              ( neg-leq-ℝ (neg-ℝ w) (max-ℝ (neg-ℝ x) (neg-ℝ y)) -w≤max))
            ( z≤min)
      in (case x (leq-left-max-ℝ _ _) , case y (leq-right-max-ℝ _ _))

  abstract
    leq-min-leq-leq-ℝ :
      {l3 : Level} (z : ℝ l3) → leq-ℝ z x → leq-ℝ z y → leq-ℝ z (min-ℝ x y)
    leq-min-leq-leq-ℝ z x≤z y≤z =
      forward-implication (is-greatest-binary-lower-bound-min-ℝ z) (x≤z , y≤z)

The binary minimum is a binary lower bound

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

  abstract
    leq-left-min-ℝ : leq-ℝ (min-ℝ x y) x
    leq-left-min-ℝ =
      pr1
        ( is-binary-lower-bound-is-greatest-binary-lower-bound-Large-Poset
          ( ℝ-Large-Poset)
          ( x)
          ( y)
          ( is-greatest-binary-lower-bound-min-ℝ x y))

    leq-right-min-ℝ : leq-ℝ (min-ℝ x y) y
    leq-right-min-ℝ =
      pr2
        ( is-binary-lower-bound-is-greatest-binary-lower-bound-Large-Poset
          ( ℝ-Large-Poset)
          ( x)
          ( y)
          ( is-greatest-binary-lower-bound-min-ℝ x y))

The large poset of real numbers has meets

has-meets-ℝ-Large-Poset : has-meets-Large-Poset ℝ-Large-Poset
meet-has-meets-Large-Poset has-meets-ℝ-Large-Poset = min-ℝ
is-greatest-binary-lower-bound-meet-has-meets-Large-Poset
  has-meets-ℝ-Large-Poset = is-greatest-binary-lower-bound-min-ℝ

The real numbers at a specific universe level are a meet semilattice

ℝ-Order-Theoretic-Meet-Semilattice :
  (l : Level) → Order-Theoretic-Meet-Semilattice (lsuc l) l
ℝ-Order-Theoretic-Meet-Semilattice l =
  ( ℝ-Poset l , λ x y → (min-ℝ x y , is-greatest-binary-lower-bound-min-ℝ x y))

For any ε : ℚ⁺, (x < min-ℝ x y + ε) ∨ (y < min-ℝ x y + ε)

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

  opaque
    unfolding min-ℝ

    approximate-above-min-ℝ :
      (ε : ℚ⁺) →
      type-disjunction-Prop
        ( le-prop-ℝ x (min-ℝ x y +ℝ real-ℚ⁺ ε))
        ( le-prop-ℝ y (min-ℝ x y +ℝ real-ℚ⁺ ε))
    approximate-above-min-ℝ ε =
      let
        case :
          {l : Level} → (w : ℝ l) →
          le-ℝ (max-ℝ (neg-ℝ x) (neg-ℝ y) -ℝ real-ℚ⁺ ε) (neg-ℝ w) →
          le-ℝ w (min-ℝ x y +ℝ real-ℚ⁺ ε)
        case w max-ε<-w =
          binary-tr le-ℝ
            ( neg-neg-ℝ w)
            ( distributive-neg-diff-ℝ _ _ ∙ commutative-add-ℝ _ _)
            ( neg-le-ℝ _ (neg-ℝ w) max-ε<-w)
      in
        elim-disjunction
          ( (le-prop-ℝ x (min-ℝ x y +ℝ real-ℚ⁺ ε)) ∨
            (le-prop-ℝ y (min-ℝ x y +ℝ real-ℚ⁺ ε)))
          ( λ max-ε<-x → inl-disjunction (case x max-ε<-x))
          ( λ max-ε<-y → inr-disjunction (case y max-ε<-y))
          ( approximate-below-max-ℝ (neg-ℝ x) (neg-ℝ y) ε)

Recent changes