English
If the chart e belongs to the maximal atlas and the point x lies in its source, then ContMDiffWithinAt is equivalent to the corresponding lifted expression in the extended atlas.
Русский
Если граф e принадлежит максимальному атласу и точка x лежит в области определения, то ContMDiffWithinAt эквивалентно соответствующему перенесенному выражению в расширенном атласе.
LaTeX
$$ContMDiffWithinAt I I' n f s x \iff ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x)$$
Lean4
theorem contMDiffAt_iff_target {x : M} :
ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (extChartAt I' (f x) ∘ f) x := by
rw [ContMDiffAt, ContMDiffAt, contMDiffWithinAt_iff_target, continuousWithinAt_univ]
