extChartAt_target_subset_range — Mathlib

English

Around the image of a point in the source, the neighborhoods are the same within extChartAt I x .target and within range I.

Русский

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

LaTeX

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

Lean4

theorem extChartAt_target_subset_range (x : M) : (extChartAt I x).target ⊆ range I := by simp only [mfld_simps]

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