The binary minimum of nonnegative real numbers

Content created by Louis Wasserman.

Created on 2026-02-15.
Last modified on 2026-02-15.

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

module real-numbers.binary-minimum-nonnegative-real-numbers where
Imports 
open import foundation.dependent-pair-types
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.binary-minimum-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.rational-real-numbers

Idea

The minimum of two nonnegative real numbers is nonnegative.

Definition

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

  abstract
    is-nonnegative-min-real-ℝ⁰⁺ : is-nonnegative-ℝ (min-ℝ x y)
    is-nonnegative-min-real-ℝ⁰⁺ = leq-min-leq-leq-ℝ x y zero-ℝ 0≤x 0≤y

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

Properties

The binary minimum is a greatest lower bound

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

  abstract
    is-greatest-binary-lower-bound-min-ℝ⁰⁺ :
      is-greatest-binary-lower-bound-Large-Poset
        ( large-poset-ℝ⁰⁺)
        ( x⁰⁺)
        ( y⁰⁺)
        ( min-ℝ⁰⁺ x⁰⁺ y⁰⁺)
    is-greatest-binary-lower-bound-min-ℝ⁰⁺ (z , _) =
      is-greatest-binary-lower-bound-min-ℝ x y z

The large poset of nonnegative real numbers has meets

has-meets-large-poset-ℝ⁰⁺ : has-meets-Large-Poset large-poset-ℝ⁰⁺
has-meets-large-poset-ℝ⁰⁺ =
  λ where
    .meet-has-meets-Large-Poset → min-ℝ⁰⁺
    .is-greatest-binary-lower-bound-meet-has-meets-Large-Poset →
      is-greatest-binary-lower-bound-min-ℝ⁰⁺

The nonnegative real numbers at a universe level form a meet-semilattice

order-theoretic-meet-semilattice-ℝ⁰⁺ :
  (l : Level) → Order-Theoretic-Meet-Semilattice (lsuc l) l
pr1 (order-theoretic-meet-semilattice-ℝ⁰⁺ l) = poset-ℝ⁰⁺ l
pr2 (order-theoretic-meet-semilattice-ℝ⁰⁺ l) x y =
  ( min-ℝ⁰⁺ x y , is-greatest-binary-lower-bound-min-ℝ⁰⁺ x y)

See also

Recent changes