The minimum of positive rational numbers

Content created by Louis Wasserman.

Created on 2025-10-04.
Last modified on 2025-10-17.

module elementary-number-theory.minimum-positive-rational-numbers where
Imports 
open import elementary-number-theory.inequality-positive-rational-numbers
open import elementary-number-theory.minimum-rational-numbers
open import elementary-number-theory.positive-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-positive-rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.dependent-pair-types
open import foundation.identity-types

open import order-theory.decidable-total-orders

Idea

The minimum of two positive rational numbers is the smallest of the two.

Definition

abstract
  is-positive-min-ℚ :
    {p q : ℚ} → is-positive-ℚ p → is-positive-ℚ q → is-positive-ℚ (min-ℚ p q)
  is-positive-min-ℚ {p} {q} is-pos-p is-pos-q =
    is-positive-le-zero-ℚ
      ( le-min-le-both-ℚ zero-ℚ p q
        ( le-zero-is-positive-ℚ is-pos-p)
        ( le-zero-is-positive-ℚ is-pos-q))

min-ℚ⁺ : ℚ⁺ → ℚ⁺ → ℚ⁺
min-ℚ⁺ (p , is-pos-p) (q , is-pos-q) =
  ( min-ℚ p q , is-positive-min-ℚ is-pos-p is-pos-q)

Properties

The binary minimum is associative

abstract
  associative-min-ℚ⁺ :
    (x y z : ℚ⁺) → min-ℚ⁺ (min-ℚ⁺ x y) z ＝ min-ℚ⁺ x (min-ℚ⁺ y z)
  associative-min-ℚ⁺ (x , _) (y , _) (z , _) = eq-ℚ⁺ (associative-min-ℚ x y z)

The binary minimum is commutative

abstract
  commutative-min-ℚ⁺ : (x y : ℚ⁺) → min-ℚ⁺ x y ＝ min-ℚ⁺ y x
  commutative-min-ℚ⁺ (x , _) (y , _) = eq-ℚ⁺ (commutative-min-ℚ x y)

The binary minimum is idempotent

abstract
  idempotent-min-ℚ⁺ : (x : ℚ⁺) → min-ℚ⁺ x x ＝ x
  idempotent-min-ℚ⁺ (x , _) = eq-ℚ⁺ (idempotent-min-ℚ x)

The binary minimum is a lower bound

abstract
  leq-left-min-ℚ⁺ : (x y : ℚ⁺) → leq-ℚ⁺ (min-ℚ⁺ x y) x
  leq-left-min-ℚ⁺ (x , _) (y , _) = leq-left-min-ℚ x y

  leq-right-min-ℚ⁺ : (x y : ℚ⁺) → leq-ℚ⁺ (min-ℚ⁺ x y) y
  leq-right-min-ℚ⁺ (x , _) (y , _) = leq-right-min-ℚ x y

Any two positive rational numbers have a positive rational number strictly less than both

module _
  (x y : ℚ⁺)
  where

  mediant-zero-min-ℚ⁺ : ℚ⁺
  mediant-zero-min-ℚ⁺ = mediant-zero-ℚ⁺ (min-ℚ⁺ x y)

  abstract
    le-left-mediant-zero-min-ℚ⁺ : le-ℚ⁺ mediant-zero-min-ℚ⁺ x
    le-left-mediant-zero-min-ℚ⁺ =
      concatenate-le-leq-ℚ
        ( rational-ℚ⁺ mediant-zero-min-ℚ⁺)
        ( rational-ℚ⁺ (min-ℚ⁺ x y))
        ( rational-ℚ⁺ x)
        ( le-mediant-zero-ℚ⁺ (min-ℚ⁺ x y))
        ( leq-left-min-ℚ⁺ x y)

    le-right-mediant-zero-min-ℚ⁺ : le-ℚ⁺ mediant-zero-min-ℚ⁺ y
    le-right-mediant-zero-min-ℚ⁺ =
      concatenate-le-leq-ℚ
        ( rational-ℚ⁺ mediant-zero-min-ℚ⁺)
        ( rational-ℚ⁺ (min-ℚ⁺ x y))
        ( rational-ℚ⁺ y)
        ( le-mediant-zero-ℚ⁺ (min-ℚ⁺ x y))
        ( leq-right-min-ℚ⁺ x y)

Recent changes