map_nhds_eq

Mathlib.Topology.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousAlgEquiv.map_nhds_eq

English

Neighborhood filters are preserved by the map: map e (nhds a) = nhds (e a).

Русский

Фильтры окрестностей сохраняются отображением: e(𝓝(a)) = 𝓝(e(a)).

LaTeX

$$$ \text{Filter.map } e \ \left(\mathcal{N}(a)\right) = \mathcal{N}(e(a)) $$$

Lean4

theorem map_nhds_eq (e : A ≃A[R] B) (a : A) : Filter.map e (𝓝 a) = 𝓝 (e a) :=
  e.toHomeomorph.map_nhds_eq a

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

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

Разделы

Аффилиация

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