isOpen_biInter_finset — Mathlib

English

For a finite set s, and f: s → Set X with each f(i) open, the iterated intersection over i in s of f(i) is open.

Русский

Для конечного множества s и отображения f: s → Set X, если каждый f(i) открыт, то последовательность пересечений открыта.

LaTeX

$$$s.Finite \rightarrow (\forall i \in s, IsOpen (f i)) \rightarrow IsOpen (\bigcap i \in s, f i)$$$

Lean4

theorem isOpen_biInter_finset {s : Finset α} {f : α → Set X} (h : ∀ i ∈ s, IsOpen (f i)) : IsOpen (⋂ i ∈ s, f i) :=
  s.finite_toSet.isOpen_biInter h

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