map_extend_symm_nhdsWithin — Mathlib

English

The nhdsWithin at a point along the inverse extension map equals the nhdsWithin at the original point with the preimage of the subset under the inverse chart. This captures the compatibility of inverse extensions with neighborhoods.

Русский

Окрестности nhdsWithin в точке, рассчитанные через обратное продолжение, равны окрестностям в исходной точке по предобразу под обратной картой.

LaTeX

$$$\\mathrm{map}\\!\\left(f^{\\mathrm{ext}}\\right)\\!\\big(\\mathcal{N}_{[(f^{\\mathrm{ext}})^{-1} s]}(f^{\\mathrm{ext}} y)\\big) = \\mathcal{N}_{s}(y)$$$

Lean4

theorem map_extend_symm_nhdsWithin {y : M} (hy : y ∈ f.source) :
    map (f.extend I).symm (𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I y) = 𝓝[s] y :=
  by
  rw [← map_extend_nhdsWithin f hy, map_map, Filter.map_congr, map_id]
  exact (f.extend I).leftInvOn.eqOn.eventuallyEq_of_mem (extend_source_mem_nhdsWithin _ hy)

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