English
A countable intersection of analytic sets is analytic. If ι is nonempty and countable and α is a T2 space, then the intersection over n of s(n) analytic implies AnalyticSet(⋂ n, s(n)).
Русский
Счетное пересечение аналитических множеств аналитично. Пусть ι непусто и счетно, пространство α т2, тогда ⋂n s(n) аналитично.
LaTeX
$$$[h_\iota : Nonempty ι][Countable ι][T2Space α] \; {s : ι → Set α} \; (\forall n, AnalyticSet (s n)) \\Rightarrow \\ AnalyticSet(\bigcap_{n} s(n)).$$$
Lean4
/-- A countable intersection of analytic sets is analytic. -/
theorem iInter [hι : Nonempty ι] [Countable ι] [T2Space α] {s : ι → Set α} (hs : ∀ n, AnalyticSet (s n)) :
AnalyticSet (⋂ n, s n) :=
by
rcases hι with
⟨i₀⟩
/- For the proof, write each `s n` as the continuous image under a map `f n` of a
Polish space `β n`. The product space `γ = Π n, β n` is also Polish, and so is the subset
`t` of sequences `x n` for which `f n (x n)` is independent of `n`. The set `t` is Polish, and
the range of `x ↦ f 0 (x 0)` on `t` is exactly `⋂ n, s n`, so this set is analytic. -/
choose β hβ h'β f f_cont f_range using fun n => analyticSet_iff_exists_polishSpace_range.1 (hs n)
let γ := ∀ n, β n
let t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
have t_closed : IsClosed t := by
apply isClosed_iInter
intro n
exact isClosed_eq ((f_cont n).comp (continuous_apply n)) ((f_cont i₀).comp (continuous_apply i₀))
haveI : PolishSpace t := t_closed.polishSpace
let F : t → α := fun x => f i₀ ((x : γ) i₀)
have F_cont : Continuous F := (f_cont i₀).comp ((continuous_apply i₀).comp continuous_subtype_val)
have F_range : range F = ⋂ n : ι, s n := by
apply Subset.antisymm
· rintro y ⟨x, rfl⟩
refine mem_iInter.2 fun n => ?_
have : f n ((x : γ) n) = F x := (mem_iInter.1 x.2 n :)
rw [← this, ← f_range n]
exact mem_range_self _
· intro y hy
have A : ∀ n, ∃ x : β n, f n x = y := by
intro n
rw [← mem_range, f_range n]
exact mem_iInter.1 hy n
choose x hx using A
have xt : x ∈ t := by
refine mem_iInter.2 fun n => ?_
simp [γ, hx]
refine ⟨⟨x, xt⟩, ?_⟩
exact hx i₀
rw [← F_range]
exact analyticSet_range_of_polishSpace F_cont
