[Merged by Bors] - refactor(Probability/Kernel/CondCdf): mv atBot_le_nhds_bot/top

Mathlib/Probability/Kernel/CondCdf.lean

@@ -66,27 +66,6 @@ theorem Real.iInter_Iic_rat : ⋂ r : ℚ, Iic (r : ℝ) = ∅ := by
   exact exists_rat_lt x
 #align real.Inter_Iic_rat Real.iInter_Iic_rat
 
--- todo after the port: move to order/filter/at_top_bot
-theorem atBot_le_nhds_bot {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderBot α]
-    [OrderTopology α] : (atBot : Filter α) ≤ 𝓝 ⊥ := by
-  cases subsingleton_or_nontrivial α
-  · simp only [nhds_discrete, le_pure_iff, mem_atBot_sets, mem_singleton_iff,
-      eq_iff_true_of_subsingleton, imp_true_iff, exists_const]
-  have h : atBot.HasBasis (fun _ : α => True) Iic := @atBot_basis α _ _
-  have h_nhds : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a => Iio a := @nhds_bot_basis α _ _ _ _ _
-  intro s
-  rw [h.mem_iff, h_nhds.mem_iff]
-  rintro ⟨a, ha_bot_lt, h_Iio_a_subset_s⟩
-  refine' ⟨⊥, trivial, _root_.trans _ h_Iio_a_subset_s⟩
-  simpa only [Iic_bot, singleton_subset_iff, mem_Iio]
-#align at_bot_le_nhds_bot atBot_le_nhds_bot
-
--- todo after the port: move to order/filter/at_top_bot
-theorem atTop_le_nhds_top {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderTop α]
-    [OrderTopology α] : (atTop : Filter α) ≤ 𝓝 ⊤ :=
-  @atBot_le_nhds_bot αᵒᵈ _ _ _ _
-#align at_top_le_nhds_top atTop_le_nhds_top
-
 end AuxLemmasToBeMoved
 
 namespace MeasureTheory.Measure

Mathlib/Topology/Order/Basic.lean

@@ -1330,6 +1330,23 @@ theorem Dense.topology_eq_generateFrom [DenselyOrdered α] {s : Set α} (hs : De
       let _ := generateFrom (Ioi '' s ∪ Iio '' s)
       exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1
 
+theorem atBot_le_nhds_bot [OrderBot α] : (atBot : Filter α) ≤ 𝓝 ⊥ := by
+  cases subsingleton_or_nontrivial α
+  · simp only [nhds_discrete, le_pure_iff, mem_atBot_sets, mem_singleton_iff,
+      eq_iff_true_of_subsingleton, imp_true_iff, exists_const]
+  have h : atBot.HasBasis (fun _ : α => True) Iic := @atBot_basis α _ _
+  have h_nhds : (𝓝 ⊥).HasBasis (fun a : α => ⊥ < a) fun a => Iio a := @nhds_bot_basis α _ _ _ _ _
+  intro s
+  rw [h.mem_iff, h_nhds.mem_iff]
+  rintro ⟨a, ha_bot_lt, h_Iio_a_subset_s⟩
+  refine' ⟨⊥, trivial, _root_.trans _ h_Iio_a_subset_s⟩
+  simpa only [Iic_bot, singleton_subset_iff, mem_Iio]
+#align at_bot_le_nhds_bot atBot_le_nhds_bot
+
+theorem atTop_le_nhds_top [OrderTop α] : (atTop : Filter α) ≤ 𝓝 ⊤ :=
+  @atBot_le_nhds_bot αᵒᵈ _ _ _ _
+#align at_top_le_nhds_top atTop_le_nhds_top
+
 variable (α)
 
 /-- Let `α` be a densely ordered linear order with order topology. If `α` is a separable space, then