The maximum of nonnegative rational numbers

Content created by Louis Wasserman.

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

module elementary-number-theory.maximum-nonnegative-rational-numbers where
Imports 
open import elementary-number-theory.inequality-nonnegative-rational-numbers
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.maximum-rational-numbers
open import elementary-number-theory.nonnegative-rational-numbers
open import elementary-number-theory.rational-numbers

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

Idea

The maximum of two nonnegative rational numbers is the greatest rational number of the two.

Definition

abstract
  is-nonnegative-max-ℚ :
    {p q : ℚ} → is-nonnegative-ℚ p → is-nonnegative-ℚ q →
    is-nonnegative-ℚ (max-ℚ p q)
  is-nonnegative-max-ℚ {p} {q} is-nonneg-p _ =
    is-nonnegative-leq-zero-ℚ
      ( transitive-leq-ℚ
        ( zero-ℚ)
        ( p)
        ( max-ℚ p q)
        ( leq-left-max-ℚ p q)
        ( leq-zero-is-nonnegative-ℚ is-nonneg-p))

max-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
max-ℚ⁰⁺ (p , is-nonneg-p) q⁰⁺@(q , is-nonneg-q) =
  (max-ℚ p q , is-nonnegative-max-ℚ is-nonneg-p is-nonneg-q)

Properties

The binary maximum is associative

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

The binary maximum is commutative

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

The binary maximum is idempotent

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

The binary maximum is an upper bound

abstract
  leq-left-max-ℚ⁰⁺ : (x y : ℚ⁰⁺) → leq-ℚ⁰⁺ x (max-ℚ⁰⁺ x y)
  leq-left-max-ℚ⁰⁺ _ _ = leq-left-max-ℚ _ _

  leq-right-max-ℚ⁰⁺ : (x y : ℚ⁰⁺) → leq-ℚ⁰⁺ y (max-ℚ⁰⁺ x y)
  leq-right-max-ℚ⁰⁺ _ _ = leq-right-max-ℚ _ _

Recent changes