nhds_ofAdd

Mathlib.Topology.Constructions

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

English

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

Русский

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

LaTeX

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

Lean4

theorem nhds_ofAdd (x : X) : 𝓝 (ofAdd x) = map ofAdd (𝓝 x) :=
  rfl

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

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

Разделы

Аффилиация

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