map_nhdsWithin_preimage_eq — Mathlib

English

For x in the source and s subset of Y, map e of nhdsWithin x (preimage e x s) equals nhdsWithin s of e(x).

Русский

Для x из источника и s подмножества Y, образ nhdsWithin x от предобраза e⁻¹(s) равен nhdsWithin s в e(x).

LaTeX

$$$ map\\; e\\; (\\mathcal{N}_{\\![ e^{-1}'(s) \\!] }(x)) = \\mathcal{N}_{s}(e(x)) $$$

Lean4

theorem map_nhdsWithin_preimage_eq {x} (hx : x ∈ e.source) (s : Set Y) : map e (𝓝[e ⁻¹' s] x) = 𝓝[s] e x := by
  rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
    e.nhdsWithin_target_inter (e.map_source hx)]

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