English
The kernel of a product is the product of kernels: nhdsKer(s × t) = nhdsKer(s) × nhdsKer(t).
Русский
Ядро произведения равняется произведению ядер: nhdsKer(s × t) = nhdsKer(s) × nhdsKer(t).
LaTeX
$$$nhdsKer(s \\times t) = nhdsKer(s) \\times nhdsKer(t)$$$
Lean4
theorem nhdsKer_prod {Y : Type*} [TopologicalSpace Y] (s : Set X) (t : Set Y) :
nhdsKer (s ×ˢ t) = nhdsKer s ×ˢ nhdsKer t :=
calc
_ = ⋃ (p ∈ s ×ˢ t), nhdsKer { p } := by conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]
_ = ⋃ (p ∈ s ×ˢ t), nhdsKer { p.1 } ×ˢ nhdsKer { p.2 } := by congr! with ⟨x, y⟩ _; rw [nhdsKer_pair]
_ = (⋃ x ∈ s, nhdsKer { x }) ×ˢ (⋃ y ∈ t, nhdsKer { y }) :=
(biUnion_prod s t (fun x => nhdsKer { x }) (fun y => nhdsKer { y }))
_ = nhdsKer s ×ˢ nhdsKer t := by simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]
