sInter — Mathlib

English

A countable intersection of Gδ sets is a Gδ set.

Русский

Счетное пересечение Gδ множеств является Gδ.

LaTeX

$$$\\forall S: Set(Set X),\\ (\\forall s\\in S, IsGδ(s)) \\land S.Countable \\Rightarrow IsGδ(\\bigcap_0 S)$$$

Lean4

/-- A countable intersection of Gδ sets is a Gδ set. -/
theorem sInter {S : Set (Set X)} (h : ∀ s ∈ S, IsGδ s) (hS : S.Countable) : IsGδ (⋂₀ S) := by
  simpa only [sInter_eq_biInter] using IsGδ.biInter hS h

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