map_mul_left_nhds₀ — Mathlib

English

If a ≠ 0 in a GroupWithZero with continuous multiplication, left translation by a sends neighborhoods of b to neighborhoods of ab: the pushforward of nhds b under x ↦ a x equals nhds (a b).

Русский

Если a ≠ 0 в группе с нулём, где умножение непрерывно, то левая трансляция на a отправляет окрестности точки b в окрестности ab: образ nhds b при отображении x ↦ a x равен nhds (a b).

LaTeX

$$$\\operatorname{map}(a \\cdot)(\\mathcal{N}(b)) = \\mathcal{N}(a b)$$$

Lean4

theorem map_mul_left_nhds₀ (ha : a ≠ 0) (b : G₀) : map (a * ·) (𝓝 b) = 𝓝 (a * b) :=
  (Homeomorph.mulLeft₀ a ha).map_nhds_eq b

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