symm_map_nhds_eq — Mathlib

English

Let e be a continuous algebra equivalence A ≃A[R] B. Then for every a in A, the neighborhood filter at a is obtained by pushing forward the neighborhood filter at e(a) through the inverse map e^{-1}. In symbols: Filter.map(e^{-1})(𝓝(e(a))) = 𝓝(a).

Русский

Пусть e — непрерывное алгебраическое эквивалентное отображение A ≃A[R] B. Тогда для любого a ∈ A окрестности a получаются как образ окрестностей e(a) под обратной картой e^{-1}. Обозначения: Filter.map(e^{-1})(𝓝(e(a))) = 𝓝(a).

LaTeX

$$$\operatorname{Filter.map}(e^{-1})(\mathcal{N}(e(a))) = \mathcal{N}(a)$$$

Lean4

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

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