English
If B is an exposed subset of A and B is nonempty, then there exist a linear functional l and a scalar a such that B = { x ∈ A | a ≤ l x }.
Русский
Если B является не пустым экспонированным подмножеством A, то существуют линейный функционал l и число a такие, что B = { x ∈ A | a ≤ l x }.
LaTeX
$$$\\exists l:\\ StrongDual 𝕜 E,\\; \\exists a:\\; E\\text{(scalar)},\\; B = \\{ x\\in A \\mid a \\le l x\\}.$$$
Lean4
/-- If `B` is a nonempty exposed subset of `A`, then `B` is the intersection of `A` with some closed
half-space. The converse is *not* true. It would require that the corresponding open half-space
doesn't intersect `A`. -/
theorem eq_inter_halfSpace' {A B : Set E} (hAB : IsExposed 𝕜 A B) (hB : B.Nonempty) :
∃ l : StrongDual 𝕜 E, ∃ a, B = {x ∈ A | a ≤ l x} :=
by
obtain ⟨l, rfl⟩ := hAB hB
obtain ⟨w, hw⟩ := hB
exact
⟨l, l w, Subset.antisymm (fun x hx => ⟨hx.1, hx.2 w hw.1⟩) fun x hx => ⟨hx.1, fun y hy => (hw.2 y hy).trans hx.2⟩⟩
