feat: special case of Disjoint.exists_open_convexes for a closed set and a singleton (#24259)

Author: YaelDillies

Mathlib/Topology/Algebra/Module/LocallyConvex.lean

@@ -127,11 +127,11 @@ theorem LocallyConvexSpace.convex_open_basis_zero [LocallyConvexSpace 𝕜 E] :
         interior_subset⟩)
     fun s hs => ⟨s, ⟨hs.2.1.mem_nhds hs.1, hs.2.2⟩, subset_rfl⟩
 
-variable {𝕜 E}
+variable {𝕜 E} [LocallyConvexSpace 𝕜 E] {s t : Set E} {x : E}
 
-/-- In a locally convex space, if `s`, `t` are disjoint convex sets, `s` is compact and `t` is
-closed, then we can find open disjoint convex sets containing them. -/
-theorem Disjoint.exists_open_convexes [LocallyConvexSpace 𝕜 E] {s t : Set E} (disj : Disjoint s t)
+/-- In a locally convex space, every two disjoint convex sets such that one is compact and the other
+is closed admit disjoint convex open neighborhoods. -/
+theorem Disjoint.exists_open_convexes (disj : Disjoint s t)
     (hs₁ : Convex 𝕜 s) (hs₂ : IsCompact s) (ht₁ : Convex 𝕜 t) (ht₂ : IsClosed t) :
     ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := by
   letI : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
@@ -145,6 +145,13 @@ theorem Disjoint.exists_open_convexes [LocallyConvexSpace 𝕜 E] {s t : Set E}
   simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
   exact hV
 
+/-- In a locally convex space, every point `x` and closed convex set `s ∌ x` admit disjoint convex
+open neighborhoods. -/
+lemma exists_open_convex_of_not_mem (hx : x ∉ s) (hsconv : Convex 𝕜 s) (hsclosed : IsClosed s) :
+    ∃ U V : Set E,
+      IsOpen U ∧ IsOpen V ∧ Convex 𝕜 U ∧ Convex 𝕜 V ∧ x ∈ U ∧ s ⊆ V ∧ Disjoint U V := by
+  simpa [*] using Disjoint.exists_open_convexes (s := {x}) (t := s) (𝕜 := 𝕜)
+
 end LinearOrderedField
 
 section LatticeOps