English
If S is convex closed and T is compact convex with S ∩ T = ∅ and disjointness, there exist f ∈ StrongDual 𝕜 E and u < v separating S and T with - the compact set property yields two thresholds u and v such that for a ∈ S, Re f(a) < u and for b ∈ T, v < Re f(b).
Русский
Если S выпукло-замкнуто и T компактно выпукло и S и T не пересекаются, существует f ∈ StrongDual 𝕜 E и u < v, которые разделяют S и T: для a ∈ S выполняется Re f(a) < u, для b ∈ T выполняется v < Re f(b).
LaTeX
$$$\exists f : StrongDual 𝕜 E, \exists u < v \in \mathbb{R}, (\forall a ∈ s, Re f(a) < u) ∧ (\forall b ∈ t, v < Re f(b))$$$
Lean4
theorem geometric_hahn_banach_closed_point (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) (disj : x ∉ s) :
∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < re (f x) :=
let ⟨f, s, _t, ha, hst, hb⟩ :=
geometric_hahn_banach_closed_compact hs₁ hs₂ (convex_singleton x) isCompact_singleton
(disjoint_singleton_right.2 disj)
⟨f, s, ha, hst.trans <| hb x <| mem_singleton _⟩
