isClosed_sInter — Mathlib

English

If every member of a collection S of subsets is closed, then the intersection of all members is closed.

Русский

Если для каждого множества t ∈ S множеств подмножества X верно, что t замкнуто, то пересечение всех t ∈ S замкнуто.

LaTeX

$$$\left( \forall t \in s, \operatorname{IsClosed}(t) \right) \Rightarrow \operatorname{IsClosed}(\bigcap_0 s)$$$

Lean4

theorem isClosed_sInter {s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s) := by
  simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion

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