feat(Order/Interval/Set/Disjoint): generalize ⋃ x ∈ s, Iic x = Iic a from LinearOrder to Preorder (#42512)

and add an `IsLeast` version.

Author: SnirBroshi

Mathlib/Order/Bounds/Basic.lean

@@ -268,6 +268,14 @@ theorem Set.Nonempty.bddAbove_lowerBounds (hs : s.Nonempty) : BddAbove (lowerBou
 theorem IsLeast.isGLB (h : IsLeast s a) : IsGLB s a :=
   ⟨h.2, fun _ hb => hb h.1⟩
 
+@[to_dual]
+theorem IsGLB.isLeast (h : IsGLB s a) (hmem : a ∈ s) : IsLeast s a :=
+  ⟨hmem, h.left⟩
+
+@[to_dual]
+theorem isLeast_iff_isGLB_and_mem : IsLeast s a ↔ IsGLB s a ∧ a ∈ s :=
+  ⟨fun h ↦ ⟨h.isGLB, h.left⟩, fun ⟨h, hmem⟩ ↦ h.isLeast hmem⟩
+
 @[to_dual]
 theorem IsLUB.upperBounds_eq (h : IsLUB s a) : upperBounds s = Ici a :=
   Set.ext fun _ => ⟨fun hb => h.2 hb, fun hb => upperBounds_mono_mem hb h.1⟩

Mathlib/Order/Interval/Set/Disjoint.lean

@@ -169,6 +169,36 @@ end Set
 
 section UnionIxx
 
+section Preorder
+
+variable [Preorder α] {s : Set α} {a : α}
+
+@[to_dual]
+theorem IsLeast.biUnion_Ici_eq_Ici (h : IsLeast s a) : ⋃ x ∈ s, Ici x = Ici a := by
+  refine (iUnion₂_subset fun x hx ↦ ?_).antisymm fun x hx ↦ mem_iUnion₂.mpr ⟨a, h.left, hx⟩
+  exact Ici_subset_Ici.mpr <| mem_lowerBounds.mp h.right x hx
+
+@[to_dual (attr := deprecated IsLeast.biUnion_Ici_eq_Ici (since := "2026-08-13"))]
+theorem IsGLB.biUnion_Ici_eq_Ici (a_glb : IsGLB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Ici x = Ici a :=
+  a_glb.isLeast a_mem |>.biUnion_Ici_eq_Ici
+
+end Preorder
+
+section PartialOrder
+
+variable [PartialOrder α] {s : Set α} {a : α}
+
+@[to_dual]
+theorem biUnion_Ici_eq_Ici_iff : ⋃ x ∈ s, Ici x = Ici a ↔ IsLeast s a := by
+  refine ⟨fun h ↦ ?_, IsLeast.biUnion_Ici_eq_Ici⟩
+  have hlb : a ∈ lowerBounds s := fun b hbs ↦ h.le <| mem_biUnion hbs self_mem_Ici
+  have ⟨b, hbs, hba⟩ := mem_iUnion₂.mp <| h.ge self_mem_Ici
+  exact ⟨hlb hbs |>.antisymm hba ▸ hbs, hlb⟩
+
+end PartialOrder
+
+section LinearOrder
+
 variable [LinearOrder α] {s : Set α} {a : α} {f : ι → α}
 
 theorem IsGLB.biUnion_Ioi_eq (h : IsGLB s a) : ⋃ x ∈ s, Ioi x = Ioi a := by
@@ -202,19 +232,10 @@ theorem IsGLB.biUnion_Ici_eq_Ioi (a_glb : IsGLB s a) (a_notMem : a ∉ s) :
     rw [mem_iUnion₂]
     exact ⟨y, hys, hyx.le⟩
 
-theorem IsGLB.biUnion_Ici_eq_Ici (a_glb : IsGLB s a) (a_mem : a ∈ s) :
-    ⋃ x ∈ s, Ici x = Ici a := by
-  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
-  · exact Ici_subset_Ici.mpr (mem_lowerBounds.mp a_glb.1 x hx)
-  · exact mem_iUnion₂.mpr ⟨a, a_mem, hx⟩
-
 theorem IsLUB.biUnion_Iic_eq_Iio (a_lub : IsLUB s a) (a_notMem : a ∉ s) :
     ⋃ x ∈ s, Iic x = Iio a :=
   a_lub.dual.biUnion_Ici_eq_Ioi a_notMem
 
-theorem IsLUB.biUnion_Iic_eq_Iic (a_lub : IsLUB s a) (a_mem : a ∈ s) : ⋃ x ∈ s, Iic x = Iic a :=
-  a_lub.dual.biUnion_Ici_eq_Ici a_mem
-
 theorem iUnion_Ici_eq_Ioi_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R}
     (no_least_elem : ⨅ i, f i ∉ range f) : ⋃ i : ι, Ici (f i) = Ioi (⨅ i, f i) := by
   simp only [← IsGLB.biUnion_Ici_eq_Ioi (@isGLB_iInf _ _ _ f) no_least_elem, mem_range,
@@ -224,12 +245,11 @@ theorem iUnion_Iic_eq_Iio_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R
     (no_greatest_elem : (⨆ i, f i) ∉ range f) : ⋃ i : ι, Iic (f i) = Iio (⨆ i, f i) :=
   @iUnion_Ici_eq_Ioi_iInf ι (OrderDual R) _ f no_greatest_elem
 
-theorem iUnion_Ici_eq_Ici_iInf {R : Type*} [CompleteLinearOrder R] {f : ι → R}
+theorem iUnion_Ici_eq_Ici_iInf {R : Type*} [CompleteLattice R] {f : ι → R}
     (has_least_elem : (⨅ i, f i) ∈ range f) : ⋃ i : ι, Ici (f i) = Ici (⨅ i, f i) := by
-  simp only [← IsGLB.biUnion_Ici_eq_Ici (@isGLB_iInf _ _ _ f) has_least_elem, mem_range,
-    iUnion_exists, iUnion_iUnion_eq']
+  simp [← isGLB_iInf.isLeast has_least_elem |>.biUnion_Ici_eq_Ici]
 
-theorem iUnion_Iic_eq_Iic_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R}
+theorem iUnion_Iic_eq_Iic_iSup {R : Type*} [CompleteLattice R] {f : ι → R}
     (has_greatest_elem : (⨆ i, f i) ∈ range f) : ⋃ i : ι, Iic (f i) = Iic (⨆ i, f i) :=
   @iUnion_Ici_eq_Ici_iInf ι (OrderDual R) _ f has_greatest_elem
 
@@ -250,4 +270,6 @@ theorem iInter_Iio_of_not_bddBelow_range (hf : ¬ BddBelow (range f)) : ⋂ i, I
   gcongr
   exact Iio_subset_Iic_self
 
+end LinearOrder
+
 end UnionIxx