English
A set is Gδ if and only if it can be written as the intersection over n of open sets f(n).
Русский
Множество является Gδ тогда и только тогда, когда его можно записать как пересечение по n открытых множеств f(n).
LaTeX
$$$IsGδ(s)\\iff \\exists f: \\mathbb{N}\\to Set(X), (\\forall n, IsOpen(f(n))) \\land s=\\bigcap_{n} f(n)$$$
Lean4
theorem isGδ_iff_eq_iInter_nat {s : Set X} : IsGδ s ↔ ∃ (f : ℕ → Set X), (∀ n, IsOpen (f n)) ∧ s = ⋂ n, f n :=
by
refine ⟨?_, ?_⟩
· rintro ⟨T, hT, T_count, rfl⟩
rcases Set.eq_empty_or_nonempty T with rfl | hT
· exact ⟨fun _n ↦ univ, fun _n ↦ isOpen_univ, by simp⟩
· obtain ⟨f, hf⟩ : ∃ (f : ℕ → Set X), T = range f := Countable.exists_eq_range T_count hT
exact ⟨f, by simp_all, by simp [hf]⟩
· rintro ⟨f, hf, rfl⟩
exact .iInter_of_isOpen hf
