map_mul_left_nhds_one₀ — Mathlib

English

For a ≠ 0, the image of the neighborhood of 1 under left translation by a equals the neighborhood of a: map (a ·) (𝓝 1) = 𝓝 a.

Русский

Для a ≠ 0 образ окрестности единицы под левой трансляцией на a равен окрестности a: map (a ·) (𝓝 1) = 𝓝 a.

LaTeX

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

Lean4

theorem map_mul_left_nhds_one₀ (ha : a ≠ 0) : map (a * ·) (𝓝 1) = 𝓝 (a) := by rw [map_mul_left_nhds₀ ha, mul_one]

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