English
The function written in the extended chart around x, with respect to I and I', acts as a translation between coordinate representations: it maps a point in the chart to the corresponding coordinate in the target chart.
Русский
Функция, записанная в расширенной карте вокруг точки x, переводит точку между координатными представлениями: она отображает точку в координаты целевой карты.
LaTeX
$$$writtenInExtChartAt I x y := \mathrm{extChartAt} I' (f x) \circ f \circ (\mathrm{extChartAt} I x)^{-1}(y)$$$
Lean4
/-- Conjugating a function to write it in the preferred charts around `x`.
The manifold derivative of `f` will just be the derivative of this conjugated function. -/
@[simp, mfld_simps]
def writtenInExtChartAt (x : M) (f : M → M') : E → E' :=
extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm
