Minimum and maximum on the lower, upper, and usual Dedekind real numbers

src/elementary-number-theory.lagda.md

@@ -97,10 +97,12 @@ open import elementary-number-theory.kolakoski-sequence public
 open import elementary-number-theory.legendre-symbol public
 open import elementary-number-theory.lower-bounds-natural-numbers public
 open import elementary-number-theory.maximum-natural-numbers public
+open import elementary-number-theory.maximum-rational-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public
 open import elementary-number-theory.mediant-integer-fractions public
 open import elementary-number-theory.mersenne-primes public
 open import elementary-number-theory.minimum-natural-numbers public
+open import elementary-number-theory.minimum-rational-numbers public
 open import elementary-number-theory.minimum-standard-finite-types public
 open import elementary-number-theory.modular-arithmetic public
 open import elementary-number-theory.modular-arithmetic-standard-finite-types public

src/elementary-number-theory/maximum-rational-numbers.lagda.md

@@ -0,0 +1,116 @@
+# Maximum on the rational numbers
+
+```agda
+module elementary-number-theory.maximum-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "maximum" Disambiguation="of pairs of rational numbers" Agda=max-ℚ}}
+of two [rational numbers](elementary-number-theory.rational-numbers.md) is the
+[greatest](elementary-number-theory.inequality-rational-numbers.md) rational
+number of the two. This is the
+[binary least upper bound](order-theory.least-upper-bounds-posets.md) in the
+[total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md).
+
+## Definition
+
+```agda
+max-ℚ : ℚ → ℚ → ℚ
+max-ℚ = max-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+## Properties
+
+### Associativity of the maximum operation
+
+```agda
+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
+
+```agda
+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
+
+```agda
+idempotent-max-ℚ : (x : ℚ) → max-ℚ x x ＝ x
+idempotent-max-ℚ =
+  idempotent-max-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+### The maximum is an upper bound
+
+```agda
+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`
+
+```agda
+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
+
+```agda
+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`
+
+```agda
+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
+```

src/elementary-number-theory/minimum-rational-numbers.lagda.md

@@ -0,0 +1,117 @@
+# Minimum on the rational numbers
+
+```agda
+module elementary-number-theory.minimum-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+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
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "minimum" Disambiguation="of pairs of rational numbers" Agda=min-ℚ}}
+of two [rational numbers](elementary-number-theory.rational-numbers.md) is the
+[smallest](elementary-number-theory.inequality-rational-numbers.md) rational
+number of the two. This is the
+[binary greatest lower bound](order-theory.greatest-lower-bounds-posets.md) in
+the
+[total order of rational numbers](elementary-number-theory.decidable-total-order-rational-numbers.md).
+
+## Definition
+
+```agda
+min-ℚ : ℚ → ℚ → ℚ
+min-ℚ = min-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+## Properties
+
+### Associativity of the minimum operation
+
+```agda
+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
+```
+
+### Commutativity of the minimum operation
+
+```agda
+commutative-min-ℚ : (x y : ℚ) → min-ℚ x y ＝ min-ℚ y x
+commutative-min-ℚ =
+  commutative-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+### The minimum operation is idempotent
+
+```agda
+idempotent-min-ℚ : (x : ℚ) → min-ℚ x x ＝ x
+idempotent-min-ℚ =
+  idempotent-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+### The minimum is a lower bound
+
+```agda
+leq-left-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ x
+leq-left-min-ℚ = leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+
+leq-right-min-ℚ : (x y : ℚ) → min-ℚ x y ≤-ℚ y
+leq-right-min-ℚ = leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+### If `a` is less than or equal to `b`, then the minimum of `a` and `b` is `a`
+
+```agda
+left-leq-right-min-ℚ : (x y : ℚ) → leq-ℚ x y → min-ℚ x y ＝ x
+left-leq-right-min-ℚ =
+  left-leq-right-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+
+right-leq-left-min-ℚ : (x y : ℚ) → leq-ℚ y x → min-ℚ x y ＝ y
+right-leq-left-min-ℚ =
+  right-leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order
+```
+
+### If `z` is less than both `x` and `y`, it is less than their minimum
+
+```agda
+le-min-le-both-ℚ : (z x y : ℚ) → le-ℚ z x → le-ℚ z y → le-ℚ z (min-ℚ x y)
+le-min-le-both-ℚ z x y z<x z<y with decide-le-leq-ℚ x y
+... | inl x<y =
+  inv-tr
+    ( le-ℚ z)
+    ( left-leq-right-min-Decidable-Total-Order
+      ( ℚ-Decidable-Total-Order)
+      ( x)
+      ( y)
+      ( leq-le-ℚ {x} {y} x<y))
+    ( z<x)
+... | inr y≤x =
+  inv-tr
+    ( le-ℚ z)
+    ( right-leq-left-min-Decidable-Total-Order ℚ-Decidable-Total-Order x y y≤x)
+    ( z<y)
+```
+
+### If `a ≤ b` and `c ≤ d`, then `min a c ≤ min b d`
+
+```agda
+min-leq-leq-ℚ :
+  (a b c d : ℚ) → leq-ℚ a b → leq-ℚ c d → leq-ℚ (min-ℚ a c) (min-ℚ b d)
+min-leq-leq-ℚ = min-leq-leq-Decidable-Total-Order ℚ-Decidable-Total-Order
+```

src/order-theory/decidable-total-orders.lagda.md

@@ -14,8 +14,10 @@ open import foundation.decidable-propositions
 open import foundation.dependent-pair-types
 open import foundation.empty-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.propositions
 open import foundation.sets
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
 open import order-theory.decidable-posets
@@ -474,3 +476,33 @@ module _
   ... | inl x≤y = antisymmetric-leq-Decidable-Total-Order T y x H x≤y
   ... | inr y<x = refl
 ```
+
+### If `a ≤ b` and `c ≤ d`, then `min a c ≤ min b d`
+
+```agda
+  min-leq-leq-Decidable-Total-Order :
+    (a b c d : type-Decidable-Total-Order T) →
+    leq-Decidable-Total-Order T a b → leq-Decidable-Total-Order T c d →
+    leq-Decidable-Total-Order
+      ( T)
+      ( min-Decidable-Total-Order T a c)
+      ( min-Decidable-Total-Order T b d)
+  min-leq-leq-Decidable-Total-Order =
+    meet-leq-leq-Order-Theoretic-Meet-Semilattice
+      ( order-theoretic-meet-semilattice-Decidable-Total-Order)
+```
+
+### If `a ≤ b` and `c ≤ d`, then `max a c ≤ max b d`
+
+```agda
+  max-leq-leq-Decidable-Total-Order :
+    (a b c d : type-Decidable-Total-Order T) →
+    leq-Decidable-Total-Order T a b → leq-Decidable-Total-Order T c d →
+    leq-Decidable-Total-Order
+      ( T)
+      ( max-Decidable-Total-Order T a c)
+      ( max-Decidable-Total-Order T b d)
+  max-leq-leq-Decidable-Total-Order =
+    join-leq-leq-Order-Theoretic-Join-Semilattice
+      ( order-theoretic-join-semilattice-Decidable-Total-Order)
+```

src/order-theory/join-semilattices.lagda.md

@@ -236,6 +236,48 @@ module _
             by ap (join-Join-Semilattice x) K
           ＝ z
             by H)
+
+  leq-left-join-Join-Semilattice :
+    (a b : type-Join-Semilattice) →
+    leq-Join-Semilattice a (join-Join-Semilattice a b)
+  leq-left-join-Join-Semilattice a b =
+    equational-reasoning
+      a ∨ (a ∨ b)
+      ＝ (a ∨ a) ∨ b by inv (associative-join-Join-Semilattice a a b)
+      ＝ a ∨ b by ap (_∨ b) (idempotent-join-Join-Semilattice a)
+
+  leq-right-join-Join-Semilattice :
+    (a b : type-Join-Semilattice) →
+    leq-Join-Semilattice b (join-Join-Semilattice a b)
+  leq-right-join-Join-Semilattice a b =
+    equational-reasoning
+      b ∨ (a ∨ b)
+      ＝ (a ∨ b) ∨ b by commutative-join-Join-Semilattice _ _
+      ＝ a ∨ (b ∨ b) by associative-join-Join-Semilattice a b b
+      ＝ a ∨ b by ap (a ∨_) (idempotent-join-Join-Semilattice b)
+
+  join-leq-leq-Join-Semilattice :
+    (a b c d : type-Join-Semilattice) →
+    leq-Join-Semilattice a b → leq-Join-Semilattice c d →
+    leq-Join-Semilattice (join-Join-Semilattice a c) (join-Join-Semilattice b d)
+  join-leq-leq-Join-Semilattice a b c d a≤b c≤d =
+    forward-implication
+      ( is-least-binary-upper-bound-join-Join-Semilattice
+        ( a)
+        ( c)
+        ( join-Join-Semilattice b d))
+      ( transitive-leq-Join-Semilattice
+          ( a)
+          ( b)
+          ( b ∨ d)
+          ( leq-left-join-Join-Semilattice b d)
+          ( a≤b) ,
+        transitive-leq-Join-Semilattice
+          ( c)
+          ( d)
+          ( b ∨ d)
+          ( leq-right-join-Join-Semilattice b d)
+          ( c≤d))
 ```
 
 ### The predicate on posets of being a join-semilattice
@@ -412,6 +454,32 @@ module _
         ( y)
         ( z))
       ( H , K)
+
+  join-leq-leq-Order-Theoretic-Join-Semilattice :
+    (a b c d : type-Order-Theoretic-Join-Semilattice) →
+    leq-Order-Theoretic-Join-Semilattice a b →
+    leq-Order-Theoretic-Join-Semilattice c d →
+    leq-Order-Theoretic-Join-Semilattice
+      ( join-Order-Theoretic-Join-Semilattice a c)
+      ( join-Order-Theoretic-Join-Semilattice b d)
+  join-leq-leq-Order-Theoretic-Join-Semilattice a b c d a≤b c≤d =
+    forward-implication
+      ( is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice
+        ( a)
+        ( c)
+        ( b ∨ d))
+      ( transitive-leq-Order-Theoretic-Join-Semilattice
+          ( a)
+          ( b)
+          ( b ∨ d)
+          ( leq-left-join-Order-Theoretic-Join-Semilattice b d)
+          ( a≤b) ,
+        transitive-leq-Order-Theoretic-Join-Semilattice
+          ( c)
+          ( d)
+          ( b ∨ d)
+          ( leq-right-join-Order-Theoretic-Join-Semilattice b d)
+          ( c≤d))
 ```
 
 ## Properties