closedConvexHull_eq_closure_convexHull

English

Under suitable conditions, the closed convex hull of s equals the closure of the convex hull of s.

Русский

При подходящих условиях замкнутая выпуклая оболочка s совпадает с замыканием выпуклой оболочки s.

LaTeX

$$closedConvexHull 𝕜 s = closure (convexHull 𝕜 s)$$

Lean4

theorem closedConvexHull_eq_closure_convexHull {s : Set E} : closedConvexHull 𝕜 s = closure (convexHull 𝕜 s) :=
  subset_antisymm
    (closedConvexHull_min (subset_trans (subset_convexHull 𝕜 s) subset_closure) (Convex.closure (convex_convexHull 𝕜 s))
      isClosed_closure)
    (closure_minimal convexHull_subset_closedConvexHull isClosed_closedConvexHull)

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