map_nhds_eq — Mathlib

English

The image of nhds under φ.leftFun equals the nhds of φ.leftFun φ.pt.

Русский

Образ окрестностей под действием φ.leftFun совпадает с окрестностями φ.leftFun φ.pt.

LaTeX

$$map φ.leftFun (𝓝 φ.pt) = 𝓝 (φ.leftFun φ.pt)$$

Lean4

theorem map_nhds_eq : map φ.leftFun (𝓝 φ.pt) = 𝓝 (φ.leftFun φ.pt) :=
  show map (Prod.fst ∘ φ.prodFun) (𝓝 φ.pt) = 𝓝 (φ.prodFun φ.pt).1 by
    rw [← map_map, φ.hasStrictFDerivAt.map_nhds_eq_of_equiv, map_fst_nhds]

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