writtenInExtChartAt_chartAt_symm_comp

English

If y lies in the target of the chart extChartAt I x, then writtenInExtChartAt I I x (chartAt H' x x) (chartAt H' x).symm y = y; compatibility with chartAt is preserved under composition.

Русский

Если y принадлежит цели extChartAt I x, то writtenInExtChartAt I I x (chartAt H' x x) (chartAt H' x).symm y = y; совместимость сохраняется при композиции.

LaTeX

$$$writtenInExtChartAt I I (chartAt H' x x) (chartAt H' x).symm y = y$ for $y$ in the target of extChartAt I x.$$

Lean4

theorem writtenInExtChartAt_chartAt_symm_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 (chartAt H' x x) (chartAt H' x).symm y) =
      y :=
  by
  letI := ChartedSpace.comp H H' M'
  simp_all only [mfld_simps, chartAt_comp]

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