extChartAt_target_eventuallyEq — Mathlib

English

Around the image of the base point, (extChartAt I x).target and range I coincide locally.

Русский

В окрестности образа базовой точки extChartAt I x .target и range I совпадают локально.

LaTeX

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

Lean4

/-- Around the image of the base point, `(extChartAt I x).target` and `range I` coincide locally. -/
theorem extChartAt_target_eventuallyEq {x : M} : (extChartAt I x).target =ᶠ[𝓝 (extChartAt I x x)] range I :=
  nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq x)

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