English
If h is a diffeomorphism M ≃⟮I,J⟯ N of class n, then differentiability of f ∘ h on s at x is equivalent to differentiability of f on h^{-1}(s) at h(x), with parameter m ≤ n.
Русский
Если h — диффеоморфизм M ≃⟮I,J⟯ N класса n, то дифференцируемость f ∘ h на s в точке x эквивалентна дифференцируемости f на h^{-1}(s) в точке h(x) с параметром m ≤ n.
LaTeX
$$$\\forall m, (h: M \\to N)\\text{ } hm:\\le n:\\ ContMDiffWithinAt I I' m (f \\circ h) s x \\iff ContMDiffWithinAt J I' m f (h^{-1}[s]) (h(x))$$$
Lean4
@[simp]
theorem contMDiffWithinAt_comp_diffeomorph_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : N → M'} {s x} (hm : m ≤ n) :
ContMDiffWithinAt I I' m (f ∘ h) s x ↔ ContMDiffWithinAt J I' m f (h.symm ⁻¹' s) (h x) :=
by
constructor
· intro Hfh
rw [← h.symm_apply_apply x] at Hfh
simpa only [Function.comp_def, h.apply_symm_apply] using
Hfh.comp (h x) (h.symm.contMDiffWithinAt.of_le hm) (mapsTo_preimage _ _)
· rw [← h.image_eq_preimage]
exact fun hf => hf.comp x (h.contMDiffWithinAt.of_le hm) (mapsTo_image _ _)
