nhds_toMul — Mathlib

English

For x in Additive X, the neighborhood at x.toMul equals the pushforward by toMul of the neighborhood at x.

Русский

Для x в Additive X окрестности в x.toMul равны образу окрестностей x под действием toMul.

LaTeX

$$$\forall x \in \mathrm{Additive}\,X,\ \mathcal{N}(x^{\mathrm{toMul}}) = \operatorname{map}(\mathrm{toMul})(\mathcal{N}(x))$$$

Lean4

theorem nhds_toMul (x : Additive X) : 𝓝 x.toMul = map toMul (𝓝 x) :=
  rfl

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