English
Let X be a topological space and let toAdd: Multiplicative X → Additive X be the natural correspondence between the multiplicative and additive structures. Then for every x in Multiplicative X, the neighborhood filter of x.toAdd in Additive X equals the pushforward of the neighborhood filter of x in Multiplicative X by toAdd.
Русский
Пусть X — топологическое пространство и пусть toAdd: Multiplicative X → Additive X — естественное соответствие между мультипликативной и аддитивной структурами. Тогда для любого x ∈ Multiplicative X окрестности x.toAdd в Additive X равны образу окрестностей x в Multiplicative X под действием toAdd.
LaTeX
$$$ 𝓝( x^{Add} ) = \\operatorname{map}(\\mathrm{toAdd})( 𝓝( x ) ). $$$
Lean4
theorem nhds_toAdd (x : Multiplicative X) : 𝓝 x.toAdd = map toAdd (𝓝 x) :=
rfl
