English
A countable union of analytic sets is analytic. If s(n) are analytic for all n in a countable index, then ⋃n s(n) is analytic.
Русский
Счетное объединение аналитических множеств аналитично. Пусть каждый s(n) аналитично, тогда ⋃n s(n) аналитично.
LaTeX
$$$[Countable ι] \; {s : ι → Set α} (hs : ∀ n, AnalyticSet (s n)) : AnalyticSet(\bigcup_{n} s(n)).$$$
Lean4
/-- A countable union of analytic sets is analytic. -/
theorem iUnion [Countable ι] {s : ι → Set α} (hs : ∀ n, AnalyticSet (s n)) : AnalyticSet (⋃ n, s n) := by
/- For the proof, write each `s n` as the continuous image under a map `f n` of a
Polish space `β n`. The union space `γ = Σ n, β n` is also Polish, and the map `F : γ → α` which
coincides with `f n` on `β n` sends it to `⋃ n, s n`. -/
choose β hβ h'β f f_cont f_range using fun n => analyticSet_iff_exists_polishSpace_range.1 (hs n)
let γ := Σ n, β n
let F : γ → α := fun ⟨n, x⟩ ↦ f n x
have F_cont : Continuous F := continuous_sigma f_cont
have F_range : range F = ⋃ n, s n := by simp only [γ, F, range_sigma_eq_iUnion_range, f_range]
rw [← F_range]
exact analyticSet_range_of_polishSpace F_cont
