English
For a family of spaces X_i, the kernel over a product indexed by i satisfies nhdsKer(univ. pi s) = univ. pi (λ i, nhdsKer(s_i)).
Русский
Для семейства пространств X_i ядро над произведением по индексу i удовлетворяет nhdsKer(univ. pi s) = univ. pi (λ i, nhdsKer(s_i)).
LaTeX
$$$nhdsKer(\\mathrm{univ}.\\pi s) = \\mathrm{univ}.\\pi (\\lambda i, nhdsKer(s(i)))$$$
Lean4
theorem nhdsKer_pi {ι : Type*} {X : ι → Type*} [Π (i : ι), TopologicalSpace (X i)] (s : Π (i : ι), Set (X i)) :
nhdsKer (univ.pi s) = univ.pi (fun i => nhdsKer (s i)) :=
calc
_ = ⋃ (p ∈ univ.pi s), nhdsKer { p } := by conv_lhs => rw [← biUnion_of_singleton (univ.pi s), nhdsKer_biUnion]
_ = ⋃ (p ∈ univ.pi s), univ.pi fun i => nhdsKer {p i} := by congr! with p _; rw [nhdsKer_singleton_pi]
_ = univ.pi fun i => ⋃ x ∈ s i, nhdsKer { x } := (biUnion_univ_pi s fun i x => nhdsKer { x })
_ = univ.pi (fun i => nhdsKer (s i)) := by simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]
