English
Let t be a convex open subset of a topological vector space E and let x be a point not in t. Then there exists a continuous linear functional f on E such that the real part of f is strictly smaller at x than at every point of t: Re(f(x)) < Re(f(b)) for all b ∈ t.
Русский
Пусть t — выпуклое открытое подпространство E и x — точка, не принадлежащая t. Тогда существует непрерывный линейный функционал f на E such that вещественная часть функционала строго меньше в x, чем в каждой точке b ∈ t: Re(f(x)) < Re(f(b)) для всех b ∈ t.
LaTeX
$$$\exists f \in \mathrm{StrongDual}_{\mathbb{k}}(E), \forall b \in t:\ \operatorname{Re}(f(x)) < \operatorname{Re}(f(b)).$$$
Lean4
theorem geometric_hahn_banach_point_open (ht₁ : Convex ℝ t) (ht₂ : IsOpen t) (disj : x ∉ t) :
∃ f : StrongDual 𝕜 E, ∀ b ∈ t, re (f x) < re (f b) :=
let ⟨f, hf⟩ := geometric_hahn_banach_open_point ht₁ ht₂ disj
⟨-f, by simpa⟩
