English
If S is convex and compact and T is convex and closed, with S and T disjoint, there exist f ∈ StrongDual 𝕜 E and real u < v such that Re f(a) < u for a ∈ S, u < v, and v < Re f(b) for b ∈ T.
Русский
Пусть S выпукло и компактно, T выпукло и замкнуто, и S и T множественно не пересекаются. Тогда существует f ∈ StrongDual 𝕜 E и числа u < v такие, что Re f(a) < u при a ∈ S, и v < Re f(b) при b ∈ T, причём u < v.
LaTeX
$$\exists f : StrongDual 𝕜 E, \exists u,v ∈ \mathbb{R}, (∀ a ∈ s, Re f a < u) ∧ u < v ∧ (∀ b ∈ t, v < Re f b)$$
Lean4
theorem geometric_hahn_banach_compact_closed (hs₁ : Convex ℝ s) (hs₂ : IsCompact s) (ht₁ : Convex ℝ t)
(ht₂ : IsClosed t) (disj : Disjoint s t) :
∃ (f : StrongDual 𝕜 E) (u v : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b) :=
by
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
obtain ⟨g, u, v, h1⟩ := _root_.geometric_hahn_banach_compact_closed hs₁ hs₂ ht₁ ht₂ disj
use extendTo𝕜'ₗ g
simp only [re_extendTo𝕜'ₗ, exists_and_left]
exact ⟨u, h1.1, v, h1.2⟩
