isClosed_iInter — Mathlib

English

If for every i, f(i) is closed, then the intersection over i of f(i) is closed.

Русский

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

LaTeX

$$$\left( \forall i, \operatorname{IsClosed}(f(i)) \right) \Rightarrow \operatorname{IsClosed}(\bigcap_i f(i))$$$

Lean4

theorem isClosed_iInter {f : ι → Set X} (h : ∀ i, IsClosed (f i)) : IsClosed (⋂ i, f i) :=
  isClosed_sInter <| forall_mem_range.2 h

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