feat(Topology/Order): add more CovBy.nhdsWithin... lemmas (#18567)

- Add lemmas about `𝓝[<] a` and `𝓝[≤] a` in a `PredOrder`.
- Add lemmas about `𝓝[>] a` and `𝓝[≥] a` in a `SuccOrder`.
- Add `CovBy.nhdsWithin_Ici` and `CovBy.nhdsWithin_Iic`.
- Prove that an `OrderClosedTopology` on a linear order which is a `PredOrder` and a `SuccOrder` is discrete.
- Cleanup theorems about `OrderTopology` vs `DiscreteTopology`.

Author: urkud

Mathlib/Topology/Instances/Discrete.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.Order.SuccPred.Basic
 import Mathlib.Topology.Order.Basic
 
 /-!
@@ -42,70 +41,25 @@ theorem DiscreteTopology.secondCountableTopology_of_encodable {α : Type*}
     [TopologicalSpace α] [DiscreteTopology α] [Countable α] : SecondCountableTopology α :=
   DiscreteTopology.secondCountableTopology_of_countable
 
-theorem bot_topologicalSpace_eq_generateFrom_of_pred_succOrder {α} [LinearOrder α] [PredOrder α]
-    [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] :
-    (⊥ : TopologicalSpace α) = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a } := by
-  refine (eq_bot_of_singletons_open fun a => ?_).symm
-  have h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a) := by
-    suffices h_singleton_eq_inter' : {a} = Iic a ∩ Ici a by
-      rw [h_singleton_eq_inter', ← Ioi_pred, ← Iio_succ]
-    rw [inter_comm, Ici_inter_Iic, Icc_self a]
-  rw [h_singleton_eq_inter]
-  letI := Preorder.topology α
-  apply IsOpen.inter
-  · exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
-  · exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
-
-theorem discreteTopology_iff_orderTopology_of_pred_succ' [LinearOrder α] [PredOrder α]
-    [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : DiscreteTopology α ↔ OrderTopology α := by
-  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-  · rw [h.eq_bot]
-    exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder
-  · rw [h.topology_eq_generate_intervals]
-    exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder.symm
-
-instance (priority := 100) DiscreteTopology.orderTopology_of_pred_succ' [h : DiscreteTopology α]
-    [LinearOrder α] [PredOrder α] [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : OrderTopology α :=
-  discreteTopology_iff_orderTopology_of_pred_succ'.1 h
-
 theorem LinearOrder.bot_topologicalSpace_eq_generateFrom {α} [LinearOrder α] [PredOrder α]
     [SuccOrder α] : (⊥ : TopologicalSpace α) = generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a } := by
-  refine (eq_bot_of_singletons_open fun a => ?_).symm
-  have h_singleton_eq_inter : {a} = Iic a ∩ Ici a := by rw [inter_comm, Ici_inter_Iic, Icc_self a]
-  by_cases ha_top : IsTop a
-  · rw [ha_top.Iic_eq, inter_comm, inter_univ] at h_singleton_eq_inter
-    by_cases ha_bot : IsBot a
-    · rw [ha_bot.Ici_eq] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      -- Porting note: Specified instance for `isOpen_univ` explicitly to fix an error.
-      apply @isOpen_univ _ (generateFrom { s | ∃ a, s = Ioi a ∨ s = Iio a })
-    · rw [isBot_iff_isMin] at ha_bot
-      rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
-  · rw [isTop_iff_isMax] at ha_top
-    rw [← Iio_succ_of_not_isMax ha_top] at h_singleton_eq_inter
-    by_cases ha_bot : IsBot a
-    · rw [ha_bot.Ici_eq, inter_univ] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
-    · rw [isBot_iff_isMin] at ha_bot
-      rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter
-      rw [h_singleton_eq_inter]
-      -- Porting note: Specified instance for `IsOpen.inter` explicitly to fix an error.
-      letI := Preorder.topology α
-      apply IsOpen.inter
-      · exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
-      · exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
+  let _ := Preorder.topology α
+  have : OrderTopology α := ⟨rfl⟩
+  exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm
+
+@[deprecated (since := "2024-11-02")]
+alias bot_topologicalSpace_eq_generateFrom_of_pred_succOrder :=
+  LinearOrder.bot_topologicalSpace_eq_generateFrom
 
 theorem discreteTopology_iff_orderTopology_of_pred_succ [LinearOrder α] [PredOrder α]
     [SuccOrder α] : DiscreteTopology α ↔ OrderTopology α := by
-  refine ⟨fun h => ⟨?_⟩, fun h => ⟨?_⟩⟩
-  · rw [h.eq_bot]
-    exact LinearOrder.bot_topologicalSpace_eq_generateFrom
-  · rw [h.topology_eq_generate_intervals]
-    exact LinearOrder.bot_topologicalSpace_eq_generateFrom.symm
+  refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
+  rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_generateFrom]
+
+@[deprecated (since := "2024-11-02")]
+alias discreteTopology_iff_orderTopology_of_pred_succ' :=
+  discreteTopology_iff_orderTopology_of_pred_succ
 
-instance (priority := 100) DiscreteTopology.orderTopology_of_pred_succ [h : DiscreteTopology α]
-    [LinearOrder α] [PredOrder α] [SuccOrder α] : OrderTopology α :=
-  discreteTopology_iff_orderTopology_of_pred_succ.mp h
+instance OrderTopology.of_discreteTopology [LinearOrder α] [PredOrder α] [SuccOrder α]
+    [DiscreteTopology α] : OrderTopology α :=
+  discreteTopology_iff_orderTopology_of_pred_succ.mp ‹_›

Mathlib/Topology/Order/OrderClosed.lean

@@ -237,12 +237,16 @@ theorem Ioo_mem_nhdsWithin_Iio' (H : a < b) : Ioo a b ∈ 𝓝[<] b := by
 theorem Ioo_mem_nhdsWithin_Iio (H : b ∈ Ioc a c) : Ioo a c ∈ 𝓝[<] b :=
   mem_of_superset (Ioo_mem_nhdsWithin_Iio' H.1) <| Ioo_subset_Ioo_right H.2
 
-theorem CovBy.nhdsWithin_Iio (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
+protected theorem CovBy.nhdsWithin_Iio (h : a ⋖ b) : 𝓝[<] b = ⊥ :=
   empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Iio' h.1
 
+protected theorem PredOrder.nhdsWithin_Iio [PredOrder α] : 𝓝[<] a = ⊥ := by
+  if h : IsMin a then simp [h.Iio_eq]
+  else exact (Order.pred_covBy_of_not_isMin h).nhdsWithin_Iio
+
 theorem Ico_mem_nhdsWithin_Iio (H : b ∈ Ioc a c) : Ico a c ∈ 𝓝[<] b :=
   mem_of_superset (Ioo_mem_nhdsWithin_Iio H) Ioo_subset_Ico_self
--- Porting note (#11215): TODO: swap `'`?
+
 -- Porting note (#11215): TODO: swap `'`?
 theorem Ico_mem_nhdsWithin_Iio' (H : a < b) : Ico a b ∈ 𝓝[<] b :=
   Ico_mem_nhdsWithin_Iio ⟨H, le_rfl⟩
@@ -282,6 +286,12 @@ theorem continuousWithinAt_Ioo_iff_Iio (h : a < b) :
 #### Point included
 -/
 
+protected theorem CovBy.nhdsWithin_Iic (H : a ⋖ b) : 𝓝[≤] b = pure b := by
+  rw [← Iio_insert, nhdsWithin_insert, H.nhdsWithin_Iio, sup_bot_eq]
+
+protected theorem PredOrder.nhdsWithin_Iic [PredOrder α] : 𝓝[≤] b = pure b := by
+  rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsWithin_Iio, sup_bot_eq]
+
 theorem Ioc_mem_nhdsWithin_Iic' (H : a < b) : Ioc a b ∈ 𝓝[≤] b :=
   inter_mem (nhdsWithin_le_nhds <| Ioi_mem_nhds H) self_mem_nhdsWithin
 
@@ -446,9 +456,12 @@ theorem Ioo_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioo a c ∈ 
 theorem Ioo_mem_nhdsWithin_Ioi' {a b : α} (H : a < b) : Ioo a b ∈ 𝓝[>] a :=
   Ioo_mem_nhdsWithin_Ioi ⟨le_rfl, H⟩
 
-theorem CovBy.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ :=
+protected theorem CovBy.nhdsWithin_Ioi {a b : α} (h : a ⋖ b) : 𝓝[>] a = ⊥ :=
   empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsWithin_Ioi' h.1
 
+protected theorem SuccOrder.nhdsWithin_Ioi [SuccOrder α] : 𝓝[>] a = ⊥ :=
+  PredOrder.nhdsWithin_Iio (α := αᵒᵈ)
+
 theorem Ioc_mem_nhdsWithin_Ioi {a b c : α} (H : b ∈ Ico a c) : Ioc a c ∈ 𝓝[>] b :=
   mem_of_superset (Ioo_mem_nhdsWithin_Ioi H) Ioo_subset_Ioc_self
 
@@ -492,6 +505,12 @@ theorem continuousWithinAt_Ioo_iff_Ioi (h : a < b) :
 ### Point included
 -/
 
+protected theorem CovBy.nhdsWithin_Ici (H : a ⋖ b) : 𝓝[≥] a = pure a :=
+  H.toDual.nhdsWithin_Iic
+
+protected theorem SuccOrder.nhdsWithin_Ici [SuccOrder α] : 𝓝[≥] a = pure a :=
+  PredOrder.nhdsWithin_Iic (α := αᵒᵈ)
+
 theorem Ico_mem_nhdsWithin_Ici' (H : a < b) : Ico a b ∈ 𝓝[≥] a :=
   inter_mem_nhdsWithin _ <| Iio_mem_nhds H
 
@@ -666,7 +685,17 @@ theorem Ico_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Ico a b ∈ 𝓝 x
 theorem Icc_mem_nhds {a b x : α} (ha : a < x) (hb : x < b) : Icc a b ∈ 𝓝 x :=
   mem_of_superset (Ioo_mem_nhds ha hb) Ioo_subset_Icc_self
 
-variable [TopologicalSpace γ]
+/-- The only order closed topology on a linear order which is a `PredOrder` and a `SuccOrder`
+is the discrete topology.
+
+This theorem is not an instance,
+because it causes searches for `PredOrder` and `SuccOrder` with their `Preorder` arguments
+and very rarely matches. -/
+theorem DiscreteTopology.of_predOrder_succOrder [PredOrder α] [SuccOrder α] :
+    DiscreteTopology α := by
+  refine discreteTopology_iff_nhds.mpr fun a ↦ ?_
+  rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsWithin_Iic,
+    SuccOrder.nhdsWithin_Ioi, sup_bot_eq]
 
 end LinearOrder