English
A pointwise C^n condition can be expressed in terms of the target chart using a focus on the coordinate expression in charts to the target.
Русский
Условие $C^n$ в точке может быть выражено через целевую карту с использованием координатного выражения в графах к цели.
LaTeX
$$ContMDiffAt I I' n f x \iff ContinuousAt f x \land ContMDiffAt I 𝓘(𝕜, E') n (extChartAt I' (f x) ∘ f) x$$
Lean4
theorem contMDiffWithinAt_iff_source_of_mem_maximalAtlas [IsManifold I n M] (he : e ∈ maximalAtlas I n M)
(hx : x ∈ e.source) :
ContMDiffWithinAt I I' n f s x ↔
ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x) :=
by
have h2x := hx; rw [← e.extend_source (I := I)] at h2x
simp_rw [ContMDiffWithinAt, (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart_source he hx,
StructureGroupoid.liftPropWithinAt_self_source, e.extend_symm_continuousWithinAt_comp_right_iff,
contDiffWithinAtProp_self_source, ContDiffWithinAtProp, Function.comp, e.left_inv hx, (e.extend I).left_inv h2x]
rfl
