Maximum on the rational numbers

Content created by Louis Wasserman and Fredrik Bakke.

Created on 2025-03-24.
Last modified on 2025-03-25.

module elementary-number-theory.maximum-rational-numbers where
Imports 
open import elementary-number-theory.decidable-total-order-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.coproduct-types
open import foundation.identity-types
open import foundation.transport-along-identifications

open import order-theory.decidable-total-orders

Idea

The maximum of two rational numbers is the greatest rational number of the two. This is the binary least upper bound in the total order of rational numbers.

Definition

max-ℚ : ℚ → ℚ → ℚ
max-ℚ = max-Decidable-Total-Order ℚ-Decidable-Total-Order

Properties

Associativity of the maximum operation

abstract
  associative-max-ℚ : (x y z : ℚ) → max-ℚ (max-ℚ x y) z ＝ max-ℚ x (max-ℚ y z)
  associative-max-ℚ =
    associative-max-Decidable-Total-Order ℚ-Decidable-Total-Order

Commutativity of the maximum operation

abstract
  commutative-max-ℚ : (x y : ℚ) → max-ℚ x y ＝ max-ℚ y x
  commutative-max-ℚ =
    commutative-max-Decidable-Total-Order ℚ-Decidable-Total-Order

The maximum operation is idempotent

abstract
  idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x
  idempotent-max-ℚ =
    idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order

The maximum is an upper bound

abstract
  leq-left-max-ℚ : (x y : ℚ) → x ≤-ℚ max-ℚ x y
  leq-left-max-ℚ = leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order

  leq-right-max-ℚ : (x y : ℚ) → y ≤-ℚ max-ℚ x y
  leq-right-max-ℚ = leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order

If a is less than or equal to b, then the maximum of a and b is b

abstract
  left-leq-right-max-ℚ : (x y : ℚ) → leq-ℚ x y → max-ℚ x y ＝ y
  left-leq-right-max-ℚ =
    left-leq-right-max-Decidable-Total-Order ℚ-Decidable-Total-Order

  right-leq-left-max-ℚ : (x y : ℚ) → leq-ℚ y x → max-ℚ x y ＝ x
  right-leq-left-max-ℚ =
    right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order

If both x and y are less than z, so is their maximum

abstract
  le-max-le-both-ℚ : (z x y : ℚ) → le-ℚ x z → le-ℚ y z → le-ℚ (max-ℚ x y) z
  le-max-le-both-ℚ z x y x<z y<z with decide-le-leq-ℚ x y
  ... | inl x<y =
    inv-tr
      ( λ w → le-ℚ w z)
      ( left-leq-right-max-Decidable-Total-Order
        ( ℚ-Decidable-Total-Order)
        ( x)
        ( y)
        ( leq-le-ℚ {x} {y} x<y))
      ( y<z)
  ... | inr y≤x =
    inv-tr
      ( λ w → le-ℚ w z)
      ( right-leq-left-max-Decidable-Total-Order ℚ-Decidable-Total-Order
        ( x)
        ( y)
        ( y≤x))
      ( x<z)

If a ≤ b and c ≤ d, then max a c ≤ max b d

abstract
  max-leq-leq-ℚ :
    (a b c d : ℚ) → leq-ℚ a b → leq-ℚ c d → leq-ℚ (max-ℚ a c) (max-ℚ b d)
  max-leq-leq-ℚ = max-leq-leq-Decidable-Total-Order ℚ-Decidable-Total-Order

Recent changes