nhdsWithin_extChartAt_target_eq_of_mem

English

Around the image of the base point, the neighborhoods inside the target agree with those inside range I.

Русский

В окрестности образа базовой точки окрестности внутри target совпадают с окрестностями внутри range I.

LaTeX

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

Lean4

/-- Around a point in the target, the neighborhoods are the same within `(extChartAt I x).target`
and within `range I`. -/
theorem nhdsWithin_extChartAt_target_eq_of_mem {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) :
    𝓝[(extChartAt I x).target] z = 𝓝[range I] z :=
  by
  rw [← PartialEquiv.right_inv (extChartAt I x) hz]
  exact nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

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