nhdsKer_pair — Mathlib

English

Kernel of a pair equals the product of kernels: nhdsKer{(x,y)} = nhdsKer{x} × nhdsKer{y}.

Русский

Ядро пары равно произведению ядер: nhdsKer{(x,y)} = nhdsKer{x} × nhdsKer{y}.

LaTeX

$$$nhdsKer(\\{(x,y)\\}) = nhdsKer(\\{x\\}) \\times nhdsKer(\\{y\\})$$$

Lean4

theorem nhdsKer_pair {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) :
    nhdsKer {(x, y)} = nhdsKer { x } ×ˢ nhdsKer { y } := by
  simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_prod_eq, ker_prod]

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