comap_mk_nhds

Mathlib.Topology.Algebra.Constructions.DomMulAct

URI: https://scilib.ai/kg/mathlib#DomMulAct.comap_mk_nhds

English

For x in DomMulAct M, comap (mk) (𝓝 x) = 𝓝 (mk.symm x).

Русский

Для x в DomMulAct M, comap (mk) (𝓝 x) = 𝓝 (mk.symm x).

LaTeX

$$$$ \operatorname{comap}(\mathrm{mk}, \mathcal{N}(x)) = \mathcal{N}(\mathrm{mk}^{-1}(x)) $$$$

Lean4

@[to_additive (attr := simp)]
theorem comap_mk_nhds (x : Mᵈᵐᵃ) : comap (mk : M → Mᵈᵐᵃ) (𝓝 x) = 𝓝 (mk.symm x) :=
  mkHomeomorph.comap_nhds_eq x

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

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

Разделы

Аффилиация

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