symm_map_nhds_eq

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.symm_map_nhds_eq

← MathLib Explorer

English

The pushforward by e.symm of a neighborhood of e(x) equals the neighborhood of x.

Русский

Пушфорвард симметрии по окрестности e(x) равен окрестности x.

LaTeX

$$$\\mathrm{map}\\; e^{-1}\\; (\\mathcal{N}(e(x))) = \\mathcal{N}(x)$$$

Lean4

theorem symm_map_nhds_eq {x} (hx : x ∈ e.source) : map e.symm (𝓝 (e x)) = 𝓝 x :=
  (e.symm.map_nhds_eq <| e.map_source hx).trans <| by rw [e.left_inv hx]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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