map_mul_right_nhds — Mathlib

English

Right translation by x is a homeomorphism; map (· * x) (𝓝 y) = 𝓝 (y x).

Русский

Правая инвариантность по x — гомеоморфизм; отображение nhds сохраняет точки посредством умножения справа.

LaTeX

$$$\operatorname{map} (\cdot * x) (\mathcal{N} (y)) = \mathcal{N} (y x)$$$

Lean4

@[to_additive (attr := simp)]
theorem map_mul_right_nhds (x y : G) : map (· * x) (𝓝 y) = 𝓝 (y * x) :=
  (Homeomorph.mulRight x).map_nhds_eq y

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