English
The product of a countable family of separable spaces is separable.
Русский
Произведение счётной семейной совокупности сепарабельных пространств разделимо.
LaTeX
$$$\\forall i,\\, \\text{SeparableSpace}(X_i) \\land \\text{Countable}(\\iota) \\Rightarrow \\text{SeparableSpace}(\\prod_{i\\in\\iota} X_i)$$$
Lean4
/-- The product of a countable family of separable spaces is a separable space. -/
instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SeparableSpace (X i)] [Countable ι] :
SeparableSpace (∀ i, X i) :=
by
choose t htc htd using (exists_countable_dense <| X ·)
haveI := fun i ↦ (htc i).to_subtype
nontriviality ∀ i, X i; inhabit ∀ i, X i
classical
set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦ (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
choose y hyt hyu using this
lift y to ∀ i : I, t i using hyt
refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
simp only [f, dif_pos hi]
exact hyu ⟨i, _⟩
