writtenInExtChartAt_chartAt — Mathlib

English

When y lies in the target of extChartAt I x, the written version of the chart at chartAt H x maps y to itself, ensuring consistency of the local coordinate description with the intrinsic model.

Русский

Если y принадлежит цели extChartAt I x, то записанная версия extChartAt I x совпадает с идентичностью на chartAt H x.

LaTeX

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

Lean4

theorem writtenInExtChartAt_chartAt {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I I x (chartAt H x) y = y := by simp_all only [mfld_simps]

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