mapsTo_extChartAt — Mathlib

English

If s is contained in the source of extChartAt I x, then extChartAt I x maps s into its inverse image intersected with range I.

Русский

Если $s \\subseteq (chartAt H x).source$, то extChartAt I x отображает s в $((extChartAt I x)^{-1}[s]) \\cap \\operatorname{range} I$.

LaTeX

$$$\\operatorname{MapsTo} (\\mathrm{extChartAt} I x)\\ s\\ ((\\mathrm{extChartAt} I x).symm^{-1}\\ s \\cap \\operatorname{range} I)$$$

Lean4

theorem mapsTo_extChartAt {x : M} (hs : s ⊆ (chartAt H x).source) :
    MapsTo (extChartAt I x) s ((extChartAt I x).symm ⁻¹' s ∩ range I) :=
  mapsTo_extend _ hs

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