convexHull_convexHull_union_left — Mathlib

English

The same union property as above with roles swapped: convexHull 𝕜 (s ∪ convexHull 𝕜 t) equals convexHull 𝕜 (s ∪ t).

Русский

Та же свойство объединения с ролями поменянными: convexHull 𝕜 (s ∪ convexHull 𝕜 t) = convexHull 𝕜 (s ∪ t).

LaTeX

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

Lean4

theorem convexHull_convexHull_union_left (s t : Set E) : convexHull 𝕜 (convexHull 𝕜 s ∪ t) = convexHull 𝕜 (s ∪ t) :=
  ClosureOperator.closure_sup_closure_left _ _ _

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