nhdsKer_singleton_pi — Mathlib

English

The kernel of a singleton function equals the product of pointwise kernels: nhdsKer({p}) = univ. pi (nhdsKer({p(i)})).

Русский

Ядро единичной функции равно произведению по i ядер {p(i)}: nhdsKer({p}) = univ. pi (nhdsKer({p(i)})).

LaTeX

$$$nhdsKer(\\{ p \\}) = univ.\\pi(\\\\lambda i, nhdsKer(\\{p(i)\\}))$$$

Lean4

theorem nhdsKer_singleton_pi {ι : Type*} {X : ι → Type*} [Π (i : ι), TopologicalSpace (X i)] (p : Π (i : ι), X i) :
    nhdsKer { p } = univ.pi (fun i => nhdsKer {p i}) := by simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]

Похожие утверждения