biInter_of_isOpen — Mathlib

English

The intersection over a countable family of open sets is a Gδ set.

Русский

Пересечение счетной семейной открытых множеств является Gδ.

LaTeX

$$$I\\text{ Countable} \\Rightarrow (\\forall i\\in I, IsOpen(f(i)))\\Rightarrow IsGδ(\\bigcap_{i\\in I} f(i))$$$

Lean4

theorem biInter_of_isOpen {I : Set ι} (hI : I.Countable) {f : ι → Set X} (hf : ∀ i ∈ I, IsOpen (f i)) :
    IsGδ (⋂ i ∈ I, f i) :=
  ⟨f '' I, by rwa [forall_mem_image], hI.image _, by rw [sInter_image]⟩

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