extChartAt_target_eventuallyEq' — Mathlib

English

Around a point in the target, extChartAt I x .target and range I coincide locally.

Русский

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

LaTeX

$$$ extChartAt I x . target =^\\mathcal{N}_{(extChartAt I x).toFun y} range I \\quad (y\\in (extChartAt I x).source) $$$

Lean4

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

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