absConvexHull_add_subset — Mathlib

English

The absConvexHull of the sum s + t is contained in the sum of the absConvexHulls: absConvexHull 𝕜 (s + t) ⊆ absConvexHull 𝕜 s + absConvexHull 𝕜 t.

Русский

absConvexHull 𝕜 (s + t) ⊆ absConvexHull 𝕜 s + absConvexHull 𝕜 t.

LaTeX

$$$$ \\operatorname{absConvexHull}_{\\mathbb{k}}(s + t) \\subseteq \\operatorname{absConvexHull}_{\\mathbb{k}}(s) + \\operatorname{absConvexHull}_{\\mathbb{k}}(t). $$$$

Lean4

theorem absConvexHull_add_subset {s t : Set E} : absConvexHull 𝕜 (s + t) ⊆ absConvexHull 𝕜 s + absConvexHull 𝕜 t :=
  absConvexHull_min (add_subset_add subset_absConvexHull subset_absConvexHull)
    ⟨Balanced.add balanced_absConvexHull balanced_absConvexHull, Convex.add convex_absConvexHull convex_absConvexHull⟩

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