English
Let E be a locally convex topological vector space over 𝕜 and let x ≠ y be points in E. Then there exists a continuous linear functional f on E such that the real part of f separates x and y, i.e., Re f(x) < Re f(y).
Русский
Пусть E — локально выпуклое топологическое векторное пространство над 𝕜 и x ≠ y в E. Тогда существует непрерывная линейная функциональная отображение f на E такая, что вещественная часть значения f в x меньше, чем в y: Re f(x) < Re f(y).
LaTeX
$$$\\exists f \\in \\mathrm{StrongDual}_{\\mathbb{k}} E\\;\\text{such that}\\; \\operatorname{re}(f(x)) < \\operatorname{re}(f(y)).$$$
Lean4
theorem geometric_hahn_banach_point_point [T1Space E] (hxy : x ≠ y) : ∃ f : StrongDual 𝕜 E, re (f x) < re (f y) :=
by
obtain ⟨f, s, t, hs, st, ht⟩ :=
geometric_hahn_banach_compact_closed (𝕜 := 𝕜) (convex_singleton x) isCompact_singleton (convex_singleton y)
isClosed_singleton (disjoint_singleton.2 hxy)
exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩
