closedAbsConvexHull_eq_closure_absConvexHull

English

If s is AbsConvex, then its closure is AbsConvex as well.

Русский

Если s AbsConvex, то его замыкание тоже AbsConvex.

LaTeX

$$$$ \\operatorname{AbsConvex} 𝕜 s \\Rightarrow \\operatorname{AbsConvex} 𝕜 (\\mathrm{closure}(s)). $$$$

Lean4

theorem closedAbsConvexHull_eq_closure_absConvexHull {s : Set E} :
    closedAbsConvexHull 𝕜 s = closure (absConvexHull 𝕜 s) :=
  subset_antisymm
    (closedAbsConvexHull_min (subset_trans (subset_absConvexHull) subset_closure)
      (AbsConvex.closure absConvex_absConvexHull) isClosed_closure)
    (closure_minimal absConvexHull_subset_closedAbsConvexHull isClosed_closedAbsConvexHull)

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