biInter — Mathlib

English

The intersection of an encodable family of Gδ sets is Gδ.

Русский

Пересечение кодируемой (за счет перечислимой) семейки Gδ множеств — это Gδ.

LaTeX

$$$IsGδ\\{\\,s: ι\\,\\} (I: Set ι) \\, (I.Countable) \\Rightarrow IsGδ (Set.iInter fun i => Set.iInter (fun h => t i h))$$$

Lean4

theorem biInter {s : Set ι} (hs : s.Countable) {t : ∀ i ∈ s, Set X} (ht : ∀ (i) (hi : i ∈ s), IsGδ (t i hi)) :
    IsGδ (⋂ i ∈ s, t i ‹_›) := by
  rw [biInter_eq_iInter]
  haveI := hs.to_subtype
  exact .iInter fun x => ht x x.2

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