ext_coord_change_source — Mathlib

English

The preimage of a neighborhood under extChartAt I x is eventually equal to the intersection of the target chart's neighborhood with the preimage of the set, after pushing through the inverse chart.

Русский

Предобраз окрестности под extChartAt I x совпадает, в пределе, с пересечением окрестности целевой карты с предобразом множества, после применения обратной карты.

LaTeX

$$$((extChartAt I x).symm^{-1} s) =^{\mathcal{N}(extChartAt I x x)} (\mathrm{target} \cap (extChartAt I x)^{-1}(s)).$$$

Lean4

theorem ext_coord_change_source (x x' : M) :
    ((extChartAt I x').symm ≫ extChartAt I x).source = I '' ((chartAt H x').symm ≫ₕ chartAt H x).source :=
  extend_coord_change_source _ _

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