convexHull_convexHull_union_right

English

The convex hull of the union of s with convexHull t equals the convex hull of the union of s with t.

Русский

Выпуклая оболочка объединения s с convexHull t равна выпуклой оболочке объединения s с t.

LaTeX

$$$ (s \\cup convexHull 𝕜 t) \\subseteq convexHull 𝕜 (s \\cup t) $$$

Lean4

theorem convexHull_convexHull_union_right (s t : Set E) : convexHull 𝕜 (s ∪ convexHull 𝕜 t) = convexHull 𝕜 (s ∪ t) :=
  ClosureOperator.closure_sup_closure_right _ _ _

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