nhdsWithin_extChartAt_target_eq — Mathlib

English

If z lies in the target, then the nhds within the target of z equals the nhds within range I of z.

Русский

Если z принадлежит target, то 𝓝[(extChartAt I x).target] z = 𝓝[range I] z.

LaTeX

$$$ z \\in (extChartAt I x).target \\Rightarrow \\mathcal{N}_{(extChartAt I x).target}(z) = \\mathcal{N}_{\\mathrm{range} I}(z).$$$

Lean4

/-- Around the image of the base point, the neighborhoods are the same
within `(extChartAt I x).target` and within `range I`. -/
theorem nhdsWithin_extChartAt_target_eq (x : M) :
    𝓝[(extChartAt I x).target] (extChartAt I x) x = 𝓝[range I] (extChartAt I x) x :=
  nhdsWithin_extChartAt_target_eq' (mem_extChartAt_source x)

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