closedAbsConvexHull — Mathlib

English

Same as 52200: the intersection of AbsConvex closed sets is AbsConvex and closed.

Русский

Аналогично; пересечение AbsConvex‑замкнутых множеств сохраняет AbsConvex и замкнутость.

LaTeX

$$$$ AbsConvex 𝕜 \\left( \\bigcap_{s \\in S} s \\right) \\wedge IsClosed\\left( \\bigcap_{s \\in S} s \\right). $$$$

Lean4

/-- The absolutely convex closed hull of a set `s` is the minimal absolutely convex closed set that
includes `s`. -/
@[simps! isClosed]
def closedAbsConvexHull : ClosureOperator (Set E) :=
  .ofCompletePred (fun s => AbsConvex 𝕜 s ∧ IsClosed s) fun _ ↦ absConvex_closed_sInter

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