isClosed_biInter — Mathlib

English

If s is a set and for all i ∈ s, f(i) is closed, then the intersection over i ∈ s of f(i) is closed.

Русский

Если i ∈ s и каждое f(i) замкнуто, то пересечение по i∈s f(i) замкнуто.

LaTeX

$$$\forall i \in s, \operatorname{IsClosed}(f(i)) \Rightarrow \operatorname{IsClosed}(\bigcap i \in s, f(i))$$$

Lean4

theorem isClosed_biInter {s : Set α} {f : α → Set X} (h : ∀ i ∈ s, IsClosed (f i)) : IsClosed (⋂ i ∈ s, f i) :=
  isClosed_iInter fun i => isClosed_iInter <| h i

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