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.

theorem gc_upperBounds_lowerBounds {α : Type u_1} [Preorder α] : GaloisConnection (⇑OrderDual.toDual ∘ upperBounds) (lowerBounds ∘ ⇑OrderDual.ofDual)

@[simp]

theorem upperBounds_iUnion {α : Type u_1} [Preorder α] {ι : Sort u_2} {s : ι → Set α} : upperBounds (⋃ (i : ι), s i) = ⋂ (i : ι), upperBounds (s i)

@[simp]

theorem lowerBounds_iUnion {α : Type u_1} [Preorder α] {ι : Sort u_2} {s : ι → Set α} : lowerBounds (⋃ (i : ι), s i) = ⋂ (i : ι), lowerBounds (s i)

theorem isLUB_iUnion_iff_of_isLUB {α : Type u_1} [Preorder α] {ι : Sort u_2} {s : ι → Set α} {u : ι → α} (hs : ∀ (i : ι), IsLUB (s i) (u i)) (c : α) : IsLUB (Set.range u) c ↔ IsLUB (⋃ (i : ι), s i) c

theorem isGLB_iUnion_iff_of_isLUB {α : Type u_1} [Preorder α] {ι : Sort u_2} {s : ι → Set α} {u : ι → α} (hs : ∀ (i : ι), IsGLB (s i) (u i)) (c : α) : IsGLB (Set.range u) c ↔ IsGLB (⋃ (i : ι), s i) c