chore(Topology/Order): move&generalize 4 lemmas (#19238)

Generalize lemmas from `CompleteLinearOrder` to
`ConditionallyCompleteLattice` or `ConditionallyCompleteLinearOrder`.

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -800,7 +800,7 @@ theorem countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ {ι : Type*} {_
       simp only [fairmeas]
       rfl
     simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
-      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (0 : ℝ≥0∞) (fun n => (as_mem n).1) as_lim]
+      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]
   rw [countable_union]
   refine countable_iUnion fun n => Finite.countable ?_
   exact finite_const_le_meas_of_disjoint_iUnion₀ μ (as_mem n).1 As_mble As_disj Union_As_finite

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -411,43 +411,6 @@ theorem Monotone.map_liminf_of_continuousAt {f : R → S} (f_incr : Monotone f)
 
 end Monotone
 
-section InfiAndSupr
-
-open Topology
-
-open Filter Set
-
-variable [CompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R]
-
-theorem iInf_eq_of_forall_le_of_tendsto {x : R} {as : ι → R} (x_le : ∀ i, x ≤ as i) {F : Filter ι}
-    [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) : ⨅ i, as i = x := by
-  refine iInf_eq_of_forall_ge_of_forall_gt_exists_lt (fun i ↦ x_le i) ?_
-  apply fun w x_lt_w ↦ ‹Filter.NeBot F›.nonempty_of_mem (eventually_lt_of_tendsto_lt x_lt_w as_lim)
-
-theorem iSup_eq_of_forall_le_of_tendsto {x : R} {as : ι → R} (le_x : ∀ i, as i ≤ x) {F : Filter ι}
-    [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) : ⨆ i, as i = x :=
-  iInf_eq_of_forall_le_of_tendsto (R := Rᵒᵈ) le_x as_lim
-
-theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto (x : R) {as : ι → R} (x_lt : ∀ i, x < as i)
-    {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) :
-    ⋃ i : ι, Ici (as i) = Ioi x := by
-  have obs : x ∉ range as := by
-    intro maybe_x_is
-    rcases mem_range.mp maybe_x_is with ⟨i, hi⟩
-    simpa only [hi, lt_self_iff_false] using x_lt i
-  -- Porting note: `rw at *` was too destructive. Let's only rewrite `obs` and the goal.
-  have := iInf_eq_of_forall_le_of_tendsto (fun i ↦ (x_lt i).le) as_lim
-  rw [← this] at obs
-  rw [← this]
-  exact iUnion_Ici_eq_Ioi_iInf obs
-
-theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto (x : R) {as : ι → R} (lt_x : ∀ i, as i < x)
-    {F : Filter ι} [Filter.NeBot F] (as_lim : Filter.Tendsto as F (𝓝 x)) :
-    ⋃ i : ι, Iic (as i) = Iio x :=
-  iUnion_Ici_eq_Ioi_of_lt_of_tendsto (R := Rᵒᵈ) x lt_x as_lim
-
-end InfiAndSupr
-
 section Indicator
 
 theorem limsup_eq_tendsto_sum_indicator_nat_atTop (s : ℕ → Set α) :

Mathlib/Topology/Order/OrderClosed.lean

@@ -150,6 +150,10 @@ theorem disjoint_nhds_atBot_iff : Disjoint (𝓝 a) atBot ↔ ¬IsBot a := by
     refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
     exact isClosed_Iic.isOpen_compl.mem_nhds hb
 
+theorem IsLUB.range_of_tendsto {F : Filter β} [F.NeBot] (hle : ∀ i, f i ≤ a)
+    (hlim : Tendsto f F (𝓝 a)) : IsLUB (range f) a :=
+  ⟨forall_mem_range.mpr hle, fun _c hc ↦ le_of_tendsto' hlim fun i ↦ hc <| mem_range_self i⟩
+
 end Preorder
 
 section NoBotOrder
@@ -170,6 +174,23 @@ theorem not_tendsto_atBot_of_tendsto_nhds (hf : Tendsto f l (𝓝 a)) : ¬Tendst
 
 end NoBotOrder
 
+theorem iSup_eq_of_forall_le_of_tendsto {ι : Type*} {F : Filter ι} [Filter.NeBot F]
+    [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIicTopology α]
+    {a : α} {f : ι → α} (hle : ∀ i, f i ≤ a) (hlim : Filter.Tendsto f F (𝓝 a)) :
+    ⨆ i, f i = a :=
+  have := F.nonempty_of_neBot
+  (IsLUB.range_of_tendsto hle hlim).ciSup_eq
+
+theorem iUnion_Iic_eq_Iio_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
+    [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIicTopology α]
+    {a : α} {f : ι → α} (hlt : ∀ i, f i < a) (hlim : Tendsto f F (𝓝 a)) :
+    ⋃ i : ι, Iic (f i) = Iio a := by
+  have obs : a ∉ range f := by
+    rw [mem_range]
+    rintro ⟨i, rfl⟩
+    exact (hlt i).false
+  rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]
+
 section LinearOrder
 
 variable [TopologicalSpace α] [LinearOrder α] [ClosedIicTopology α] [TopologicalSpace β]
@@ -376,6 +397,10 @@ protected alias ⟨_, BddBelow.closure⟩ := bddBelow_closure
 theorem disjoint_nhds_atTop_iff : Disjoint (𝓝 a) atTop ↔ ¬IsTop a :=
   disjoint_nhds_atBot_iff (α := αᵒᵈ)
 
+theorem IsGLB.range_of_tendsto {F : Filter β} [F.NeBot] (hle : ∀ i, a ≤ f i)
+    (hlim : Tendsto f F (𝓝 a)) : IsGLB (range f) a :=
+  IsLUB.range_of_tendsto (α := αᵒᵈ) hle hlim
+
 end Preorder
 
 section NoTopOrder
@@ -396,6 +421,18 @@ theorem not_tendsto_atTop_of_tendsto_nhds (hf : Tendsto f l (𝓝 a)) : ¬Tendst
 
 end NoTopOrder
 
+theorem iInf_eq_of_forall_le_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
+    [ConditionallyCompleteLattice α] [TopologicalSpace α] [ClosedIciTopology α]
+    {a : α} {f : ι → α} (hle : ∀ i, a ≤ f i) (hlim : Tendsto f F (𝓝 a)) :
+    ⨅ i, f i = a :=
+  iSup_eq_of_forall_le_of_tendsto (α := αᵒᵈ) hle hlim
+
+theorem iUnion_Ici_eq_Ioi_of_lt_of_tendsto {ι : Type*} {F : Filter ι} [F.NeBot]
+    [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [ClosedIciTopology α]
+    {a : α} {f : ι → α} (hlt : ∀ i, a < f i) (hlim : Tendsto f F (𝓝 a)) :
+    ⋃ i : ι, Ici (f i) = Ioi a :=
+  iUnion_Iic_eq_Iio_of_lt_of_tendsto (α := αᵒᵈ) hlt hlim
+
 section LinearOrder
 
 variable [TopologicalSpace α] [LinearOrder α] [ClosedIciTopology α] [TopologicalSpace β]