English
A closed convex set s is the intersection of the half-spaces {x | l x ≤ l y for some y ∈ s} as l runs over all continuous linear functionals.
Русский
Замкнутое выпуклое множество s является пересечением полупространств {x | l x ≤ l y для некоторого y ∈ s} по всем непрерывным линейным функционалам l.
LaTeX
$$$\bigcap_{l} \{x \mid \exists y\in s:\; l(x) \le l(y)\} = s$$$
Lean4
/-- A closed convex set is the intersection of the half-spaces containing it. -/
theorem iInter_halfSpaces_eq (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) :
⋂ l : StrongDual ℝ E, {x | ∃ y ∈ s, l x ≤ 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).not_ge le_rfl
