map_nhds_eq_of_equiv — Mathlib

English

The push-forward of the neighborhood filter by f at a equals the neighborhood filter at f(a).

Русский

Перемещение фильтра окрестностей по f в точке a равно окрестностям в точке f(a).

LaTeX

$$$ \operatorname{map} f (\mathcal{N}(a)) = \mathcal{N}(f(a)) $$$

Lean4

theorem map_nhds_eq_of_equiv (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : map f (𝓝 a) = 𝓝 (f a) :=
  (hf.toOpenPartialHomeomorph f).map_nhds_eq hf.mem_toOpenPartialHomeomorph_source

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