absConvexHull_subset_iff — Mathlib

English

For every AbsConvex set t, the inclusion absConvexHull(s) ⊆ t is equivalent to s ⊆ t.

Русский

Для каждого AbsConvex множества t включение absConvexHull(s) ⊆ t эквивалентно s ⊆ t.

LaTeX

$$$$ \\text{If } t \\text{ is AbsConvex},\\; \\operatorname{absConvexHull}_{\\mathbb{k}}(s) \\subseteq t \\iff s \\subseteq t. $$$$

Lean4

theorem absConvexHull_subset_iff (ht : AbsConvex 𝕜 t) : absConvexHull 𝕜 s ⊆ t ↔ s ⊆ t :=
  (show (absConvexHull 𝕜).IsClosed t from ht).closure_le_iff

Похожие утверждения