feat: generalize some lemmas about linear ordered topological spaces (#33863)

Currently, lemmas about `Filter.map ((↑) : Set.Iio a → X) Filter.atTop` etc
assume that the ambient type is densely ordered.
However, it suffices to require that `a` is an `Order.IsSuccPrelimit`.

Make this generalization and move the lemmas to a new file.
Also, use the new lemmas to drop a `[DenselyOrdered _]` assumption
in one lemma in measure theory.

These more precise statements are also useful when dealing with, e.g.,
linear ordered topologies defined by ordinals.

Author: urkud

Mathlib.lean

@@ -7380,6 +7380,7 @@ public import Mathlib.Topology.OpenPartialHomeomorph.Continuity
 public import Mathlib.Topology.OpenPartialHomeomorph.Defs
 public import Mathlib.Topology.OpenPartialHomeomorph.IsImage
 public import Mathlib.Topology.Order
+public import Mathlib.Topology.Order.AtTopBotIxx
 public import Mathlib.Topology.Order.Basic
 public import Mathlib.Topology.Order.Bornology
 public import Mathlib.Topology.Order.Category.AlexDisc

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -9,6 +9,7 @@ public import Mathlib.Analysis.Complex.Asymptotics
 public import Mathlib.Analysis.Complex.Trigonometric
 public import Mathlib.Analysis.SpecificLimits.Normed
 public import Mathlib.Topology.Algebra.MetricSpace.Lipschitz
+import Mathlib.Topology.Order.AtTopBotIxx
 
 /-!
 # Complex and real exponential
@@ -300,10 +301,11 @@ theorem tendsto_div_pow_mul_exp_add_atTop (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) :
 
 /-- `Real.exp` as an order isomorphism between `ℝ` and `(0, +∞)`. -/
 def expOrderIso : ℝ ≃o Ioi (0 : ℝ) :=
-  StrictMono.orderIsoOfSurjective _ (exp_strictMono.codRestrict exp_pos) <|
+  StrictMono.orderIsoOfSurjective _
+    (exp_strictMono.codRestrict fun x ↦ Set.mem_Ioi.mpr (exp_pos x)) <|
     (continuous_exp.subtype_mk _).surjective
       (by rw [tendsto_Ioi_atTop]; simp only [tendsto_exp_atTop])
-      (by rw [tendsto_Ioi_atBot]; simp only [tendsto_exp_atBot_nhdsGT])
+      (by simp [tendsto_exp_atBot_nhdsGT])
 
 @[simp]
 theorem coe_expOrderIso_apply (x : ℝ) : (expOrderIso x : ℝ) = exp x :=

Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin
 module
 
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
+import Mathlib.Topology.Order.AtTopBotIxx
 
 /-!
 # The `arctan` function.
@@ -192,10 +193,10 @@ theorem arctan_eq_zero_iff : arctan x = 0 ↔ x = 0 :=
   .trans (by rw [arctan_zero]) arctan_injective.eq_iff
 
 theorem tendsto_arctan_atTop : Tendsto arctan atTop (𝓝[<] (π / 2)) :=
-  tendsto_Ioo_atTop.mp tanOrderIso.symm.tendsto_atTop
+  tendsto_Ioo_atTop (by simp) |>.mp tanOrderIso.symm.tendsto_atTop
 
 theorem tendsto_arctan_atBot : Tendsto arctan atBot (𝓝[>] (-(π / 2))) :=
-  tendsto_Ioo_atBot.mp tanOrderIso.symm.tendsto_atBot
+  tendsto_Ioo_atBot (by simp) |>.mp tanOrderIso.symm.tendsto_atBot
 
 theorem arctan_eq_of_tan_eq (h : tan x = y) (hx : x ∈ Ioo (-(π / 2)) (π / 2)) :
     arctan y = x :=

Mathlib/MeasureTheory/Measure/Hausdorff.lean

@@ -10,6 +10,7 @@ public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
 public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
 public import Mathlib.Topology.MetricSpace.Holder
 public import Mathlib.Topology.MetricSpace.MetricSeparated
+import Mathlib.Topology.Order.AtTopBotIxx
 
 /-!
 # Hausdorff measure and metric (outer) measures
@@ -276,7 +277,7 @@ theorem mono_pre_nat (m : Set X → ℝ≥0∞) : Monotone fun k : ℕ => pre m
 
 theorem tendsto_pre (m : Set X → ℝ≥0∞) (s : Set X) :
     Tendsto (fun r => pre m r s) (𝓝[>] 0) (𝓝 <| mkMetric' m s) := by
-  rw [← map_coe_Ioi_atBot, tendsto_map'_iff]
+  rw [← tendsto_comp_coe_Ioi_atBot]
   simp only [mkMetric', OuterMeasure.iSup_apply, iSup_subtype']
   exact tendsto_atBot_iSup fun r r' hr => mono_pre _ hr _
 

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
 public import Mathlib.MeasureTheory.Measure.NullMeasurable
 public import Mathlib.Order.Interval.Set.Monotone
+import Mathlib.Topology.Order.AtTopBotIxx
 
 /-!
 # Measure spaces
@@ -650,17 +651,21 @@ theorem exists_measure_iInter_lt {α ι : Type*} {_ : MeasurableSpace α} {μ :
 /-- The measure of the intersection of a decreasing sequence of measurable
 sets indexed by a linear order with first countable topology is the limit of the measures. -/
 theorem tendsto_measure_biInter_gt {ι : Type*} [LinearOrder ι] [TopologicalSpace ι]
-    [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] {s : ι → Set α}
+    [OrderTopology ι] [FirstCountableTopology ι] {s : ι → Set α}
     {a : ι} (hs : ∀ r > a, NullMeasurableSet (s r) μ) (hm : ∀ i j, a < i → i ≤ j → s i ⊆ s j)
     (hf : ∃ r > a, μ (s r) ≠ ∞) : Tendsto (μ ∘ s) (𝓝[Ioi a] a) (𝓝 (μ (⋂ r > a, s r))) := by
-  have : (atBot : Filter (Ioi a)).IsCountablyGenerated := by
-    rw [← comap_coe_Ioi_nhdsGT]
-    infer_instance
-  simp_rw [← map_coe_Ioi_atBot, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]
-  apply tendsto_measure_iInter_atBot
-  · rwa [Subtype.forall]
-  · exact fun i j h ↦ hm i j i.2 h
-  · simpa only [Subtype.exists, exists_prop]
+  by_cases ha : Order.IsPredPrelimit a
+  · have : (atBot : Filter (Ioi a)).IsCountablyGenerated := by
+      rw [← comap_coe_Ioi_nhdsGT a ha]
+      infer_instance
+    simp_rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, ← mem_Ioi, biInter_eq_iInter]
+    apply tendsto_measure_iInter_atBot
+    · rwa [Subtype.forall]
+    · exact fun i j h ↦ hm i j i.2 h
+    · simpa only [Subtype.exists, exists_prop]
+  · rw [Order.not_isPredPrelimit_iff_exists_covBy] at ha
+    rcases ha with ⟨b, hab⟩
+    simp [hab.nhdsGT]
 
 theorem measure_if {x : β} {t : Set β} {s : Set α} [Decidable (x ∈ t)] :
     μ (if x ∈ t then s else ∅) = indicator t (fun _ => μ s) x := by split_ifs with h <;> simp [h]

Mathlib/Topology/Order/AtTopBotIxx.lean

@@ -0,0 +1,200 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+module
+
+public import Mathlib.Topology.Order.Basic
+public import Mathlib.Order.SuccPred.Limit
+import Mathlib.Topology.Order.IsLUB
+
+/-!
+# `Filter.atTop` and `Filter.atBot` for intervals in a linear order topology
+
+Let `X` be a linear order with order topology.
+Let `a` be a point that is either the bottom element of `X` or is not isolated on the left,
+see `Order.IsSuccPrelimit`.
+Then the `Filter.atTop` filter on `Set.Iio a` and `𝓝[<] a` are related by the coercion map
+via pushforward and pullback, see `map_coe_Iio_atTop` and `comap_coe_Iio_nhdsLT`.
+
+We prove several versions of this statement for `Set.Iio`, `Set.Ioi`, and `Set.Ioo`,
+as well as `Filter.atTop` and `Filter.atBot`.
+
+The assumption on `a` is automatically satisfied for densely ordered types,
+see `Order.IsSuccPrelimit.of_dense`.
+-/
+
+public section
+
+open Set Filter Order OrderDual
+open scoped Topology
+
+variable {X : Type*} [LinearOrder X] [TopologicalSpace X] [OrderTopology X]
+  {s : Set X} {a b : X}
+
+theorem comap_coe_nhdsLT_eq_atTop_iff :
+    comap ((↑) : s → X) (𝓝[<] b) = atTop ↔
+      s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty) := by
+  rcases s.eq_empty_or_nonempty with rfl | hsne
+  · simp [eq_iff_true_of_subsingleton]
+  have := hsne.to_subtype
+  simp only [hsne, true_imp_iff]
+  by_cases hsub : s ⊆ Iio b
+  · simp only [hsub, true_and]
+    constructor
+    · intro h a ha
+      have := preimage_mem_comap (m := ((↑) : s → X)) (Ioo_mem_nhdsLT ha)
+      rw [h] at this
+      rcases Filter.nonempty_of_mem this with ⟨⟨c, hcs⟩, hc⟩
+      exact ⟨c, hcs, hc⟩
+    · intro h
+      refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_
+      · intro a hab
+        rcases h a hab with ⟨c, hcs, hc⟩
+        use ⟨c, hcs⟩
+        simp_all [subset_def, hc.1.trans_le]
+      · rintro ⟨a, has⟩ -
+        use a, hsub has
+        simp_all [subset_def, le_of_lt]
+  · suffices ¬Tendsto (↑) (atTop : Filter s) (𝓝[<] b) by
+      contrapose this
+      simp_all [tendsto_iff_comap]
+    intro h
+    rcases not_subset_iff_exists_mem_notMem.mp hsub with ⟨a, has, ha⟩
+    rcases h.eventually eventually_mem_nhdsWithin |>.and (eventually_ge_atTop ⟨a, has⟩) |>.exists
+      with ⟨⟨c, hcs⟩, hcb, hac⟩
+    apply lt_irrefl a
+    calc
+      a ≤ c := by simpa using hac
+      _ < b := by simpa using hcb
+      _ ≤ a := by simpa using ha
+
+theorem comap_coe_nhdsGT_eq_atBot_iff :
+    comap ((↑) : s → X) (𝓝[>] b) = atBot ↔
+      s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty) := by
+  refine comap_coe_nhdsLT_eq_atTop_iff (s := OrderDual.ofDual ⁻¹' s) (b := OrderDual.toDual b)
+    |>.trans <| .and .rfl <| forall₃_congr fun hne a ha ↦ ?_
+  rw [← a.toDual_ofDual, Ioo_toDual]
+  rfl
+
+theorem comap_coe_nhdsLT_of_Ioo_subset (hsb : s ⊆ Iio b) (hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s)
+    (hb : IsSuccPrelimit b := by exact .of_dense _) :
+    comap ((↑) : s → X) (𝓝[<] b) = atTop := by
+  rw [comap_coe_nhdsLT_eq_atTop_iff]
+  refine ⟨hsb, fun hsne a ha ↦ ?_⟩
+  rcases hs hsne with ⟨c, hcb, hcs⟩
+  rcases hb.lt_iff_exists_lt.mp (max_lt ha hcb) with ⟨x, hxb, hacx⟩
+  rw [max_lt_iff] at hacx
+  exact ⟨x, hcs ⟨hacx.2, hxb⟩, hacx.1, hxb⟩
+
+theorem comap_coe_nhdsGT_of_Ioo_subset (hsa : s ⊆ Ioi a) (hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s)
+    (ha : IsPredPrelimit a := by exact .of_dense _) :
+    comap ((↑) : s → X) (𝓝[>] a) = atBot := by
+  refine comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual
+  simpa only [OrderDual.exists, Ioo_toDual]
+
+theorem map_coe_atTop_of_Ioo_subset (hsb : s ⊆ Iio b) (hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s)
+    (hb : IsSuccPrelimit b := by exact .of_dense _) :
+    map ((↑) : s → X) atTop = 𝓝[<] b := by
+  rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)
+  · have : IsEmpty s := ⟨fun x => hb'.subset (hsb x.2)⟩
+    rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
+  · rw [← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb, map_comap_of_mem]
+    rw [Subtype.range_val]
+    exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)
+
+theorem map_coe_atBot_of_Ioo_subset (hsa : s ⊆ Ioi a) (hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s)
+    (ha : IsPredPrelimit a := by exact .of_dense _) :
+    map ((↑) : s → X) atBot = 𝓝[>] a := by
+  refine map_coe_atTop_of_Ioo_subset (s := ofDual ⁻¹' s) (b := toDual a) hsa ?_ ha.dual
+  intro b' hb'
+  simpa [OrderDual.exists] using hs (ofDual b') hb'
+
+/-- The `atTop` filter for an open interval `Ioo a b` comes from the left-neighbourhoods filter at
+the right endpoint in the ambient order. -/
+@[simp]
+theorem comap_coe_Ioo_nhdsLT (a b : X) (hb : IsSuccPrelimit b := by exact .of_dense _) :
+    comap ((↑) : Ioo a b → X) (𝓝[<] b) = atTop :=
+  comap_coe_nhdsLT_of_Ioo_subset Ioo_subset_Iio_self
+    (fun h => ⟨a, h.elim fun _x hx ↦ hx.1.trans hx.2, Subset.rfl⟩) hb
+
+/-- The `atBot` filter for an open interval `Ioo a b` comes from the right-neighbourhoods filter at
+the left endpoint in the ambient order. -/
+@[simp]
+theorem comap_coe_Ioo_nhdsGT (a b : X) (ha : IsPredPrelimit a := by exact .of_dense _) :
+    comap ((↑) : Ioo a b → X) (𝓝[>] a) = atBot :=
+  comap_coe_nhdsGT_of_Ioo_subset Ioo_subset_Ioi_self
+    (fun h => ⟨b, h.elim fun _x hx ↦ hx.1.trans hx.2, Subset.rfl⟩) ha
+
+@[simp]
+theorem comap_coe_Ioi_nhdsGT (a : X) (ha : IsPredPrelimit a := by exact .of_dense _) :
+    comap ((↑) : Ioi a → X) (𝓝[>] a) = atBot :=
+  comap_coe_nhdsGT_of_Ioo_subset Subset.rfl (fun ⟨x, hx⟩ => ⟨x, hx, Ioo_subset_Ioi_self⟩) ha
+
+@[simp]
+theorem comap_coe_Iio_nhdsLT (a : X) (ha : IsSuccPrelimit a := by exact .of_dense _) :
+    comap ((↑) : Iio a → X) (𝓝[<] a) = atTop :=
+  comap_coe_Ioi_nhdsGT (toDual a) ha.dual
+
+@[simp]
+theorem map_coe_Ioo_atTop (h : a < b) (hb : IsSuccPrelimit b := by exact .of_dense _) :
+    map ((↑) : Ioo a b → X) atTop = 𝓝[<] b :=
+  map_coe_atTop_of_Ioo_subset Ioo_subset_Iio_self (fun _ _ => ⟨_, h, Subset.rfl⟩) hb
+
+@[simp]
+theorem map_coe_Ioo_atBot (h : a < b) (ha : IsPredPrelimit a := by exact .of_dense _) :
+    map ((↑) : Ioo a b → X) atBot = 𝓝[>] a :=
+  map_coe_atBot_of_Ioo_subset Ioo_subset_Ioi_self (fun _ _ => ⟨_, h, Subset.rfl⟩) ha
+
+@[simp]
+theorem map_coe_Ioi_atBot (a : X) (ha : IsPredPrelimit a := by exact .of_dense _) :
+    map ((↑) : Ioi a → X) atBot = 𝓝[>] a :=
+  map_coe_atBot_of_Ioo_subset Subset.rfl (fun b hb => ⟨b, hb, Ioo_subset_Ioi_self⟩) ha
+
+@[simp]
+theorem map_coe_Iio_atTop (a : X) (ha : IsSuccPrelimit a := by exact .of_dense _) :
+    map ((↑) : Iio a → X) atTop = 𝓝[<] a :=
+  map_coe_Ioi_atBot (toDual a) ha.dual
+
+variable {α : Type*} {l : Filter α} {f : X → α}
+
+@[simp]
+theorem tendsto_comp_coe_Ioo_atTop (h : a < b) (hb : IsSuccPrelimit b := by exact .of_dense _) :
+    Tendsto (fun x : Ioo a b => f x) atTop l ↔ Tendsto f (𝓝[<] b) l := by
+  rw [← map_coe_Ioo_atTop h hb, tendsto_map'_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_comp_coe_Ioo_atBot (h : a < b) (ha : IsPredPrelimit a := by exact .of_dense _) :
+    Tendsto (fun x : Ioo a b => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
+  rw [← map_coe_Ioo_atBot h ha, tendsto_map'_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_comp_coe_Ioi_atBot (ha : IsPredPrelimit a := by exact .of_dense _) :
+    Tendsto (fun x : Ioi a => f x) atBot l ↔ Tendsto f (𝓝[>] a) l := by
+  rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_comp_coe_Iio_atTop (ha : IsSuccPrelimit a := by exact .of_dense _) :
+    Tendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l := by
+  rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_Ioo_atTop {f : α → Ioo a b} (hb : IsSuccPrelimit b := by exact .of_dense _) :
+    Tendsto f l atTop ↔ Tendsto (fun x => (f x : X)) l (𝓝[<] b) := by
+  rw [← comap_coe_Ioo_nhdsLT a b hb, tendsto_comap_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_Ioo_atBot {f : α → Ioo a b} (ha : IsPredPrelimit a := by exact .of_dense _) :
+    Tendsto f l atBot ↔ Tendsto (fun x => (f x : X)) l (𝓝[>] a) := by
+  rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_Ioi_atBot {f : α → Ioi a} (ha : IsPredPrelimit a := by exact .of_dense _) :
+    Tendsto f l atBot ↔ Tendsto (fun x => (f x : X)) l (𝓝[>] a) := by
+  rw [← comap_coe_Ioi_nhdsGT a ha, tendsto_comap_iff, Function.comp_def]
+
+@[simp]
+theorem tendsto_Iio_atTop {f : α → Iio a} (ha : IsSuccPrelimit a := by exact .of_dense _) :
+    Tendsto f l atTop ↔ Tendsto (fun x => (f x : X)) l (𝓝[<] a) := by
+  rw [← comap_coe_Iio_nhdsLT a ha, tendsto_comap_iff, Function.comp_def]