absConvex_closed_sInter — Mathlib

English

If S is a set of subsets of E such that every member is AbsConvex and closed, then the intersection ⋂ S is AbsConvex and closed.

Русский

Пусть S ‑ семейство подмножеств E, и каждый элемент S является AbsConvex и замкнут; тогда ⋂ S является AbsConvex и замкнутым.

LaTeX

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

Lean4

theorem absConvex_closed_sInter {S : Set (Set E)} (h : ∀ s ∈ S, AbsConvex 𝕜 s ∧ IsClosed s) :
    AbsConvex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S) :=
  ⟨AbsConvex.sInter (fun s hs => (h s hs).1), isClosed_sInter fun _ hs => (h _ hs).2⟩

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