feat(Order/Bounds/Lattice): bounds over collections of sets (#19150)

Some results about upper and lower bounds over collections of sets.

Inspired by #15412, but possibly of greater interest?



Co-authored-by: Christopher Hoskin <[email protected]>

Mathlib.lean

@@ -4088,6 +4088,7 @@ import Mathlib.Order.BoundedOrder.Monotone
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Order.Bounds.Defs
 import Mathlib.Order.Bounds.Image
+import Mathlib.Order.Bounds.Lattice
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Category.BddDistLat
 import Mathlib.Order.Category.BddLat

Mathlib/Order/Bounds/Basic.lean

@@ -119,6 +119,12 @@ abbrev IsGreatest.orderTop (h : IsGreatest s a) :
   top := ⟨a, h.1⟩
   le_top := Subtype.forall.2 h.2
 
+theorem isLUB_congr (h : upperBounds s = upperBounds t) : IsLUB s a ↔ IsLUB t a := by
+  rw [IsLUB, IsLUB, h]
+
+theorem isGLB_congr (h : lowerBounds s = lowerBounds t) : IsGLB s a ↔ IsGLB t a := by
+  rw [IsGLB, IsGLB, h]
+
 /-!
 ### Monotonicity
 -/

Mathlib/Order/Bounds/Lattice.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Data.Set.Lattice
+
+/-!
+# Unions and intersections of bounds
+
+Some results about upper and lower bounds over collections of sets.
+
+## Implementation notes
+
+In a separate file as we need to import `Mathlib.Data.Set.Lattice`.
+
+-/
+
+variable {α : Type*} [Preorder α] {ι : Sort*} {s : ι → Set α}
+
+open Set
+
+theorem gc_upperBounds_lowerBounds : GaloisConnection
+    (OrderDual.toDual ∘ upperBounds : Set α → (Set α)ᵒᵈ)
+    (lowerBounds ∘ OrderDual.ofDual : (Set α)ᵒᵈ → Set α) := by
+  simpa [GaloisConnection, subset_def, mem_upperBounds, mem_lowerBounds]
+    using fun S T ↦ forall₂_swap
+
+@[simp]
+theorem upperBounds_iUnion :
+    upperBounds (⋃ i, s i) = ⋂ i, upperBounds (s i) :=
+  gc_upperBounds_lowerBounds.l_iSup
+
+@[simp]
+theorem lowerBounds_iUnion :
+    lowerBounds (⋃ i, s i) = ⋂ i, lowerBounds (s i) :=
+  gc_upperBounds_lowerBounds.u_iInf
+
+theorem isLUB_iUnion_iff_of_isLUB {u : ι → α} (hs : ∀ i, IsLUB (s i) (u i)) (c : α) :
+    IsLUB (Set.range u) c ↔ IsLUB (⋃ i, s i) c := by
+  refine isLUB_congr ?_
+  simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]
+
+theorem isGLB_iUnion_iff_of_isLUB {u : ι → α} (hs : ∀ i, IsGLB (s i) (u i)) (c : α) :
+    IsGLB (Set.range u) c ↔ IsGLB (⋃ i, s i) c := by
+  refine isGLB_congr ?_
+  simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]