feat(Topology/Order): add IsMax.of_disjoint_nhds_Ioi, IsMin.of_disjoint_nhds_Iio, nonempty_nhds_inter_Ioi, nonempty_nhds_inter_Iio (leanprover-community#37550)

Add `nonempty_nhds_inter_Ioi`: a neighborhood of `x` has nonempty intersection with `Ioi x` when `x` is not a maximum.

Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project.

Co-authored-by: Leo Diedering <129694072+ldiedering@users.noreply.github.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: 3 people

Mathlib/Topology/Order/DenselyOrdered.lean

@@ -47,6 +47,26 @@ theorem closure_Iio' (h : (Iio a).Nonempty) : closure (Iio a) = Iic a :=
 theorem closure_Iio (a : α) [NoMinOrder α] : closure (Iio a) = Iic a :=
   closure_Iio' nonempty_Iio
 
+theorem IsMax.of_disjoint_nhds_Ioi {x : α} {u : Set α} (hu : u ∈ nhds x)
+    (hd : Disjoint u (Set.Ioi x)) : IsMax x := by
+  by_contra hx
+  exact (mem_closure_iff_nhds.mp (closure_Ioi' (not_isMax_iff.mp hx) ▸ self_mem_Ici) u hu).ne_empty
+    (disjoint_iff.mp hd)
+
+theorem IsMin.of_disjoint_nhds_Iio {x : α} {u : Set α} (hu : u ∈ nhds x)
+    (hd : Disjoint u (Set.Iio x)) : IsMin x :=
+  IsMax.of_disjoint_nhds_Ioi (α := αᵒᵈ) hu hd
+
+theorem nonempty_nhds_inter_Ioi {x : α} {u : Set α} (hu : u ∈ nhds x) (hx : ¬IsMax x) :
+    (u ∩ Set.Ioi x).Nonempty := by
+  by_contra h
+  exact hx (IsMax.of_disjoint_nhds_Ioi hu (Set.disjoint_iff_inter_eq_empty.mpr
+    (Set.not_nonempty_iff_eq_empty.mp h)))
+
+theorem nonempty_nhds_inter_Iio {x : α} {u : Set α} (hu : u ∈ nhds x) (hx : ¬IsMin x) :
+    (u ∩ Set.Iio x).Nonempty :=
+  nonempty_nhds_inter_Ioi (α := αᵒᵈ) hu hx
+
 /-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`. -/
 @[simp]
 theorem closure_Ioo {a b : α} (hab : a ≠ b) : closure (Ioo a b) = Icc a b := by