map_nhds_eq

Mathlib.Topology.Algebra.Module.Equiv

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

English

Repeats the nhds preservation property under the homeomorphism.

Русский

Повторение свойства сохранения nhds под гомеоморфизмом.

LaTeX

$$$ map e (\mathcal{N}(x)) = \mathcal{N}(e(x)) $$$

Lean4

theorem map_nhds_eq (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : map e (𝓝 x) = 𝓝 (e x) :=
  e.toHomeomorph.map_nhds_eq x

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

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

Разделы

Аффилиация

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