English
If every s_i is separable, then the universal product is separable.
Русский
Если каждый s_i сепарабелен, то универсальный произведение сепарабельно.
LaTeX
$$$\forall i, IsSeparable(s_i) \rightarrow IsSeparable( Set.univ.pi s )$$$
Lean4
theorem univ_pi {ι : Type*} [Countable ι] {X : ι → Type*} {s : ∀ i, Set (X i)} [∀ i, TopologicalSpace (X i)]
(h : ∀ i, IsSeparable (s i)) : IsSeparable (univ.pi s) := by
classical
rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
· rw [he]
exact countable_empty.isSeparable
· choose c c_count hc using h
haveI := fun i ↦ (c_count i).to_subtype
set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
· exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
choose f hfu hfc using H
refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
simpa only [g, dif_pos hi] using hfu i hi
intro i hi
exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2
