English
If a point x lies in the source of the chart e in the maximal atlas, then ContMDiffAt is equivalent to a lifted form in the maximal atlas with the target chart.
Русский
Если x лежит в области определения графа e в максимальном атласе, то ContMDiffAt эквивалентно переносной форме в максимальном атласе.
LaTeX
$$ContMDiffAt I I' n f x \iff ContMDiffWithinAt I I' n f s x with s = Set.univ and (e extend etc.)$$
Lean4
/-- One can reformulate being `Cⁿ` at a point as being `Cⁿ` in the source space when
composing with the extended chart. -/
theorem contMDiffAt_iff_source :
ContMDiffAt I I' n f x ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x) :=
by
rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_source]
simp
