extChartAt_preimage_mem_nhds — Mathlib

English

The nhdsWithin equality expresses that local neighborhoods are preserved when passing to the chart range via extChartAt.

Русский

Неравенство окрестностей внутри диапазона сохраняет локальные окрестности через карту extChartAt.

LaTeX

$$$\mathcal{nhdsWithin}((\mathrm{extChartAt} I x)^{-1}(s)) = \mathcal{nhdsWithin}(\mathrm{extChartAt} I x x)\,|_{\mathrm{range}(I)}.$$$

Lean4

/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
is a neighborhood of the preimage. -/
theorem extChartAt_preimage_mem_nhds {x : M} (ht : t ∈ 𝓝 x) : (extChartAt I x).symm ⁻¹' t ∈ 𝓝 ((extChartAt I x) x) :=
  by
  apply (continuousAt_extChartAt_symm x).preimage_mem_nhds
  rwa [(extChartAt I x).left_inv (mem_extChartAt_source _)]

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