English
Let 𝕜 be a field and E a vector space over 𝕜. For any subset s ⊆ E and any x ∈ E, x lies in the absolute convex hull of s if and only if x lies in every AbsConvex superset t that contains s.
Русский
Пусть 𝕜 — поле, E — векторное пространство над 𝕜. Для любой подмножества s ⊆ E и любого x ∈ E верно: x принадлежит абсолютной выпуклой оболочке s тогда и только тогда, когда x принадлежит каждому AbsConvex-надмножествоу t, содержащему s.
LaTeX
$$$$ x \\in \\operatorname{absConvexHull}_{\\mathbb{k}}(s) \\iff \\forall t,\\ s \\subseteq t \\to \\operatorname{AbsConvex} 𝕜 t \\to x \\in t. $$$$
Lean4
theorem mem_absConvexHull_iff : x ∈ absConvexHull 𝕜 s ↔ ∀ t, s ⊆ t → AbsConvex 𝕜 t → x ∈ t := by
simp_rw [absConvexHull_eq_iInter, mem_iInter]
