symm_map_nhds_eq — Mathlib

English

Let e be a continuous linear equivalence between M1 and M2. Then the pushforward of the neighborhood filter around e(x) by the inverse map e^{-1} equals the neighborhood filter around x, i.e., the inverse map preserves neighborhoods.

Русский

Пусть e — непрерывное линейное эквивалентное отображение между M1 и M2. Тогда образ фильтра окрестностей e(x) по обратному отображению e^{-1} равен окрестностям x: e^{-1}_*(𝓝_{M2}(e(x))) = 𝓝_{M1}(x).

LaTeX

$$$(e^{-1})_* \\mathcal{N}_{M_2}(e(x)) = \\mathcal{N}_{M_1}(x)$$$

Lean4

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

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