English
In a locally convex space, if x is not in a closed convex set s, then there exist disjoint open convex neighborhoods U of x and V containing s.
Русский
В локально выпуклом пространстве, если точка x не принадлежит замкнутому выпуклому множеству s, то существуют непересекающиеся открытые выпуклые окрестности U точки x и V, содержащие s.
LaTeX
$$$\text{Not}(x \in s) \Rightarrow \text{Convex}(s) \wedge \text{IsClosed}(s) \Rightarrow \exists U\exists V,\; \text{IsOpen}(U)\land \text{IsOpen}(V)\land \text{Convex}(U)\land \text{Convex}(V)\land x\in U\land s\subseteq V\land \text{Disjoint}(U,V).$$$
Lean4
/-- In a locally convex space, every point `x` and closed convex set `s ∌ x` admit disjoint convex
open neighborhoods. -/
theorem exists_open_convex_of_notMem (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) (𝕜 := 𝕜)
