nhdsWithin_extChartAt_target_eq' — Mathlib

English

Around a point in the target, the neighborhoods of extChartAt I x y inside the target equal those inside range I.

Русский

В окрестности точки в целевом диапазоне окрестности extChartAt I x y внутри target равны окрестностям внутри range I.

LaTeX

$$$\\forall x,y:(\\text{hy}): \\, \\mathcal{N}_{(extChartAt I x).target}(extChartAt I x y) = \\mathcal{N}_{\\mathrm{range} I}(extChartAt I x y).$$$

Lean4

/-- Around the image of a point in the source, the neighborhoods are the same
within `(extChartAt I x).target` and within `range I`. -/
theorem nhdsWithin_extChartAt_target_eq' {x y : M} (hy : y ∈ (extChartAt I x).source) :
    𝓝[(extChartAt I x).target] extChartAt I x y = 𝓝[range I] extChartAt I x y :=
  nhdsWithin_extend_target_eq _ <| by rwa [← extChartAt_source I]

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