closure — Mathlib

English

The closed absolute convex hull of s equals the closure of the absConvexHull of s (same as 52208).

Русский

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

LaTeX

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

Lean4

theorem closure {s : Set E} (hs : AbsConvex 𝕜 s) : AbsConvex 𝕜 (closure s) :=
  ⟨Balanced.closure hs.1, Convex.closure hs.2⟩

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