feat: ∃ᶠ x in 𝓝 a, x < a (#7941)

* Add `frequently_lt_nhds` and `frequently_gt_nhds`.
* Move some lemmas from `Topology/Order/Basic` to `Topology/Algebra/Order/LeftRight`.
* Relax TC assumptions in `Filter.Eventually.exists_lt` (and `*_gt`).
  New versions assume `NeBot (𝓝[<] a)` and `NeBot (𝓝[>] a)`,
  so the latter one can be applied, e.g., to `((a : ℝ≥0) : ℝ≥0∞)`.

From the Mandelbrot set connectedness project.

Co-Authored-By: @girving

Author: urkud

Mathlib/Topology/Algebra/Order/LeftRight.lean

@@ -27,6 +27,44 @@ left continuous, right continuous
 
 open Set Filter Topology
 
+section Preorder
+
+variable {α : Type*} [TopologicalSpace α] [Preorder α]
+
+lemma frequently_lt_nhds (a : α) [NeBot (𝓝[<] a)] : ∃ᶠ x in 𝓝 a, x < a :=
+  frequently_iff_neBot.2 ‹_›
+
+lemma frequently_gt_nhds (a : α) [NeBot (𝓝[>] a)] : ∃ᶠ x in 𝓝 a, a < x :=
+  frequently_iff_neBot.2 ‹_›
+
+theorem Filter.Eventually.exists_lt {a : α} [NeBot (𝓝[<] a)] {p : α → Prop}
+    (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b < a, p b :=
+  ((frequently_lt_nhds a).and_eventually h).exists
+#align filter.eventually.exists_lt Filter.Eventually.exists_lt
+
+theorem Filter.Eventually.exists_gt {a : α} [NeBot (𝓝[>] a)] {p : α → Prop}
+    (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b > a, p b :=
+  ((frequently_gt_nhds a).and_eventually h).exists
+#align filter.eventually.exists_gt Filter.Eventually.exists_gt
+
+theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) :=
+  nhdsWithin_neBot_of_mem H₂
+#align nhds_within_Ici_ne_bot nhdsWithin_Ici_neBot
+
+instance nhdsWithin_Ici_self_neBot (a : α) : NeBot (𝓝[≥] a) :=
+  nhdsWithin_Ici_neBot (le_refl a)
+#align nhds_within_Ici_self_ne_bot nhdsWithin_Ici_self_neBot
+
+theorem nhdsWithin_Iic_neBot {a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a) :=
+  nhdsWithin_neBot_of_mem H
+#align nhds_within_Iic_ne_bot nhdsWithin_Iic_neBot
+
+instance nhdsWithin_Iic_self_neBot (a : α) : NeBot (𝓝[≤] a) :=
+  nhdsWithin_Iic_neBot (le_refl a)
+#align nhds_within_Iic_self_ne_bot nhdsWithin_Iic_self_neBot
+
+end Preorder
+
 section PartialOrder
 
 variable {α β : Type*} [TopologicalSpace α] [PartialOrder α] [TopologicalSpace β]

Mathlib/Topology/Order/Basic.lean

@@ -276,25 +276,6 @@ theorem IsClosed.hypograph [TopologicalSpace β] {f : β → α} {s : Set β} (h
   (hs.preimage continuous_fst).isClosed_le continuousOn_snd (hf.comp continuousOn_fst Subset.rfl)
 #align is_closed.hypograph IsClosed.hypograph
 
--- Porting note: todo: move these lemmas to `Topology.Algebra.Order.LeftRight`
-theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) :=
-  nhdsWithin_neBot_of_mem H₂
-#align nhds_within_Ici_ne_bot nhdsWithin_Ici_neBot
-
-@[instance]
-theorem nhdsWithin_Ici_self_neBot (a : α) : NeBot (𝓝[≥] a) :=
-  nhdsWithin_Ici_neBot (le_refl a)
-#align nhds_within_Ici_self_ne_bot nhdsWithin_Ici_self_neBot
-
-theorem nhdsWithin_Iic_neBot {a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a) :=
-  nhdsWithin_neBot_of_mem H
-#align nhds_within_Iic_ne_bot nhdsWithin_Iic_neBot
-
-@[instance]
-theorem nhdsWithin_Iic_self_neBot (a : α) : NeBot (𝓝[≤] a) :=
-  nhdsWithin_Iic_neBot (le_refl a)
-#align nhds_within_Iic_self_ne_bot nhdsWithin_Iic_self_neBot
-
 end Preorder
 
 section PartialOrder
@@ -2477,12 +2458,6 @@ instance nhdsWithin_Ioi_self_neBot [NoMaxOrder α] (a : α) : NeBot (𝓝[>] a)
   nhdsWithin_Ioi_neBot (le_refl a)
 #align nhds_within_Ioi_self_ne_bot nhdsWithin_Ioi_self_neBot
 
-theorem Filter.Eventually.exists_gt [NoMaxOrder α] {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) :
-    ∃ b > a, p b := by
-  simpa only [exists_prop, gt_iff_lt, and_comm] using
-    ((h.filter_mono (@nhdsWithin_le_nhds _ _ a (Ioi a))).and self_mem_nhdsWithin).exists
-#align filter.eventually.exists_gt Filter.Eventually.exists_gt
-
 theorem nhdsWithin_Iio_neBot' {b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤ c) :
     NeBot (𝓝[Iio c] b) :=
   mem_closure_iff_nhdsWithin_neBot.1 <| by rwa [closure_Iio' H₁]
@@ -2500,11 +2475,6 @@ instance nhdsWithin_Iio_self_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a)
   nhdsWithin_Iio_neBot (le_refl a)
 #align nhds_within_Iio_self_ne_bot nhdsWithin_Iio_self_neBot
 
-theorem Filter.Eventually.exists_lt [NoMinOrder α] {a : α} {p : α → Prop} (h : ∀ᶠ x in 𝓝 a, p x) :
-    ∃ b < a, p b :=
-  Filter.Eventually.exists_gt (α := αᵒᵈ) h
-#align filter.eventually.exists_lt Filter.Eventually.exists_lt
-
 theorem right_nhdsWithin_Ico_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b) :=
   (isLUB_Ico H).nhdsWithin_neBot (nonempty_Ico.2 H)
 #align right_nhds_within_Ico_ne_bot right_nhdsWithin_Ico_neBot