map_mul_right_nhds₀

Mathlib.Topology.Algebra.GroupWithZero

URI: https://scilib.ai/kg/mathlib#map_mul_right_nhds₀

English

For a ≠ 0 and b ∈ G₀, the pushforward of nhds b under x ↦ x a equals nhds (b a).

Русский

Для a ≠ 0 и b ∈ G₀ образ nhds b под отображением x ↦ x a равен nhds (b a).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru