English
If s is a convex and closed subset of E, then s is exactly the intersection, over all continuous linear functionals l on E, of the half-spaces { x ∈ E | ∃ y ∈ s, Re(lx) ≤ Re(ly) }. In particular, s equals the intersection of all supporting half-spaces determined by functionals.
Русский
Пусть s ⊂ E является выпуклым и замкнутым множеством. Тогда s есть точная пересечение всех полупространств, задаваемых линейными функционалами: $$\\bigcap_{l}\\{x\\in E\\mid \\exists y\\in s: \\operatorname{Re}(l x) \\le \\operatorname{Re}(l y)\\}=s.$$
LaTeX
$$$\\displaystyle \\bigcap_{l\\in \\mathrm{StrongDual}_{\\mathbb{k}} E} \\{x\\in E \\mid \\exists\, y\\in s, \\operatorname{re}(l x) \\le \\operatorname{re}(l y)\\} = s$$$
Lean4
theorem iInter_halfSpaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
⋂ l : StrongDual 𝕜 E, {x | ∃ y ∈ s, re (l x) ≤ re (l y)} = s :=
by
rw [Set.iInter_setOf]
refine Set.Subset.antisymm (fun x hx => ?_) fun x hx l => ⟨x, hx, le_rfl⟩
by_contra h
obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point (𝕜 := 𝕜) hs₁ hs₂ h
obtain ⟨y, hy, hxy⟩ := hx l
exact ((hxy.trans_lt (hlA y hy)).trans hl).false
