closedConvexHull_closure_eq_closedConvexHull

English

The closed convex hull does not change if s is replaced by its closure.

Русский

Замкнутая выпуклая оболочка не изменяется при замыкании множества s.

LaTeX

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

Lean4

@[simp]
theorem closedConvexHull_closure_eq_closedConvexHull {s : Set E} :
    closedConvexHull 𝕜 (closure s) = closedConvexHull 𝕜 s :=
  subset_antisymm (by simpa using ((closedConvexHull 𝕜).monotone (closure_subset_closedConvexHull (𝕜 := 𝕜) (E := E))))
    ((closedConvexHull 𝕜).monotone subset_closure)

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