closedAbsConvexHull_closure_eq_closedAbsConvexHull

English

The closed absolute convex hull of s equals the closure of the absConvexHull of s.

Русский

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

LaTeX

$$$$ closedAbsConvexHull 𝕜 s = \\mathrm{closure}(absConvexHull 𝕜 s). $$$$

Lean4

@[simp]
theorem closedAbsConvexHull_closure_eq_closedAbsConvexHull {s : Set E} :
    closedAbsConvexHull 𝕜 (closure s) = closedAbsConvexHull 𝕜 s :=
  subset_antisymm
    (by simpa using ((closedAbsConvexHull 𝕜).monotone (closure_subset_closedAbsConvexHull (𝕜 := 𝕜) (E := E))))
    ((closedAbsConvexHull 𝕜).monotone subset_closure)

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