The minimum of positive rational numbers

Content created by Louis Wasserman.

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

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

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

min-ℚ⁺ : ℚ⁺ → ℚ⁺ → ℚ⁺
min-ℚ⁺ = min-Decidable-Total-Order decidable-total-order-ℚ⁺

Properties

The binary minimum is associative

abstract
  associative-min-ℚ⁺ :
    (x y z : ℚ⁺) → min-ℚ⁺ (min-ℚ⁺ x y) z ＝ min-ℚ⁺ x (min-ℚ⁺ y z)
  associative-min-ℚ⁺ =
    associative-min-Decidable-Total-Order decidable-total-order-ℚ⁺

The binary minimum is commutative

abstract
  commutative-min-ℚ⁺ : (x y : ℚ⁺) → min-ℚ⁺ x y ＝ min-ℚ⁺ y x
  commutative-min-ℚ⁺ =
    commutative-min-Decidable-Total-Order decidable-total-order-ℚ⁺

The binary minimum is idempotent

abstract
  idempotent-min-ℚ⁺ : (x : ℚ⁺) → min-ℚ⁺ x x ＝ x
  idempotent-min-ℚ⁺ =
    idempotent-min-Decidable-Total-Order decidable-total-order-ℚ⁺

The binary minimum is a lower bound

abstract
  leq-left-min-ℚ⁺ : (x y : ℚ⁺) → leq-ℚ⁺ (min-ℚ⁺ x y) x
  leq-left-min-ℚ⁺ = leq-left-min-Decidable-Total-Order decidable-total-order-ℚ⁺

  leq-right-min-ℚ⁺ : (x y : ℚ⁺) → leq-ℚ⁺ (min-ℚ⁺ x y) y
  leq-right-min-ℚ⁺ =
    leq-right-min-Decidable-Total-Order decidable-total-order-ℚ⁺

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