nhds_ofMul

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#nhds_ofMul

English

For all x in X, the neighborhood filter at ofMul(x) equals the pushforward by ofMul of the neighborhood filter at x.

Русский

Для всех x в X окрестности в точке ofMul(x) равны образу neighborhoods x под действием ofMul.

LaTeX

$$$\forall x\in X,\ \mathcal{N}(\mathrm{ofMul}(x)) = \operatorname{map}(\mathrm{ofMul})(\mathcal{N}(x))$$$

Lean4

theorem nhds_ofMul (x : X) : 𝓝 (ofMul x) = map ofMul (𝓝 x) :=
  rfl

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

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

Разделы

Аффилиация

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