English
If the y-chart target contains the image in the source of the y-chart at f(x), the equivalence expresses C^n within by targeting through the target's chart.
Русский
Если образ через граф целевого графа содержит f(x) в источнике графа цели, эквивалентность выражает $C^n$ внутри через цель графа.
LaTeX
$$contMDiffWithinAt_iff_target_of_mem_source [IsManifold I' n M'] {x : M} {y : M'} (hy : f x ∈ (chartAt H' y).source) : ContMDiffWithinAt I I' n f s x ↔ ContinuousWithinAt f s x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) s x$$
Lean4
theorem contMDiffAt_iff_target_of_mem_source [IsManifold I' n M'] {x : M} {y : M'} (hy : f x ∈ (chartAt H' y).source) :
ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) x := by
rw [ContMDiffAt, contMDiffWithinAt_iff_target_of_mem_source hy, continuousWithinAt_univ, ContMDiffAt]
