English
Let A and B be subsets of a vector space E. If B is an exposed subset of A, then B is the intersection of A with a closed half-space defined by a linear functional. More precisely, there exist a linear functional ℓ on E and a scalar a such that B = { x ∈ A : a ≤ ℓ(x) }.
Русский
Пусть A и B — подмножества пространства E. Если B является экспонированной подмножностью A, то B есть пересечение A с полупространством, заданным линейным функционалом. То есть существуют линейный функционал ℓ и число a такие, что B = { x ∈ A | a ≤ ℓ(x) }.
LaTeX
$$$$\exists \ell \in E^*, \exists a \in \mathbb{K},\ B = \{ x \in A \mid a \le \ell(x) \}. $$$$
Lean4
/-- For nontrivial `𝕜`, if `B` is an 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 [IsOrderedRing 𝕜] [Nontrivial 𝕜] {A B : Set E} (hAB : IsExposed 𝕜 A B) :
∃ l : StrongDual 𝕜 E, ∃ a, B = {x ∈ A | a ≤ l x} :=
by
obtain rfl | hB := B.eq_empty_or_nonempty
· refine ⟨0, 1, ?_⟩
rw [eq_comm, eq_empty_iff_forall_notMem]
rintro x ⟨-, h⟩
rw [ContinuousLinearMap.zero_apply] at h
have : ¬(1 : 𝕜) ≤ 0 := not_le_of_gt zero_lt_one
contradiction
exact hAB.eq_inter_halfSpace' hB
