isClosed_closedAbsConvexHull — Mathlib

English

The absolute convex hull of the closed absolute convex hull is itself absolute convex.

Русский

Абсолютно выпуклая оболочка замкнутой абсолютной выпуклой оболочки остаётся абс. выпуклой.

LaTeX

$$$$ AbsConvex 𝕜 \\left( closedAbsConvexHull 𝕜 s \\right). $$$$

Lean4

theorem isClosed_closedAbsConvexHull {s : Set E} : IsClosed (closedAbsConvexHull 𝕜 s) :=
  ((closedAbsConvexHull 𝕜).isClosed_closure s).2

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