writtenInExtChartAt_chartAt_comp — Mathlib

English

The coordinate change map between any two charts is C^n on its source domain; this is the smoothness of the transition maps in the atlas.

Русский

Переход между двумя картами гладкий класса C^n на своей области определения; гладкость переходных карт в атласе.

LaTeX

$$$\text{ContDiffOn}_{\mathbb{K}}^n(\mathrm{extChartAt} I x \circ (\mathrm{extChartAt} I x').symm) ((\mathrm{extChartAt} I x').symm \circ (\mathrm{extChartAt} I x)).\text{source}$$$

Lean4

theorem writtenInExtChartAt_chartAt_comp [ChartedSpace H H'] (x : M') {y}
    (hy :
      y ∈
        letI := ChartedSpace.comp H H' M';
        (extChartAt I x).target) :
    (letI := ChartedSpace.comp H H' M';
      writtenInExtChartAt I I x (chartAt H' x) y) =
      y :=
  by
  letI := ChartedSpace.comp H H' M'
  simp_all only [mfld_simps, chartAt_comp]

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