isOpen_iInter_of_finite — Mathlib

English

If ι is finite and each s(i) is open, then ⋂ i, s(i) is open.

Русский

Если индексы образуют конечное множество, и каждый s(i) открыт, то пересечение по i открыто.

LaTeX

$$$[Finite \ ι] \; (\forall i, IsOpen (s i)) \rightarrow IsOpen \Big(\bigcap_i s i\Big)$$$

Lean4

theorem isOpen_iInter_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsOpen (s i)) : IsOpen (⋂ i, s i) :=
  (finite_range _).isOpen_sInter (forall_mem_range.2 h)

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