English
If S and T are convex and open in a real topological vector space and disjoint, there exist a strong dual f and a real u such that re f(a) < u for all a ∈ S, and u < re f(b) for all b ∈ T.
Русский
Если S и T — выпуклые и открытые множества в вещественном топологическом векторном пространстве и несовпадающие, существует сильное двойственное отображение f и число u так, что re f(a) < u для всех a ∈ S и u < re f(b) для всех b ∈ T.
LaTeX
$$\exists f : StrongDual 𝕜 E, \exists u ∈ \mathbb{R}, (∀ a ∈ s, Re(f a) < u) ∧ ∀ b ∈ t, u < Re(f b)$$
Lean4
theorem geometric_hahn_banach_open_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (ht₁ : Convex ℝ t) (ht₃ : IsOpen t)
(disj : Disjoint s t) : ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ ∀ b ∈ t, u < re (f b) :=
by
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open_open hs₁ hs₂ ht₁ ht₃ disj
use extendTo𝕜'ₗ f
simp only [re_extendTo𝕜'ₗ]
exact Exists.intro u h
