map_nhdsWithin_eq — Mathlib

English

For any x in the source and s subset of X, map e of nhdsWithin x s equals nhdsWithin of e(x) with the image of the intersection.

Русский

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

LaTeX

$$$\\mathrm{map}\\; e\\; (\\mathcal{N}_{s}(x)) = \\mathcal{N}_{image(e)(s)}(e(x))$$$

Lean4

theorem map_nhdsWithin_eq {x} (hx : x ∈ e.source) (s : Set X) : map e (𝓝[s] x) = 𝓝[e '' (e.source ∩ s)] e x :=
  calc
    map e (𝓝[s] x) = map e (𝓝[e.source ∩ s] x) := congr_arg (map e) (e.nhdsWithin_source_inter hx _).symm
    _ = 𝓝[e '' (e.source ∩ s)] e x :=
      (e.leftInvOn.mono inter_subset_left).map_nhdsWithin_eq (e.left_inv hx)
        (e.continuousAt_symm (e.map_source hx)).continuousWithinAt (e.continuousAt hx).continuousWithinAt

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