English
If h is a n-class diffeomorphism M ≃⟮I,J⟯ N, then for any m ≤ n, and any f, the ContMDiffOn of f ∘ h equals ContMDiffOn of f with preimage sets under h.
Русский
Если h — диффеоморфизм класса n между M и N, то для любого m ≤ n справедлива эквивалентность contMDiffOn для f ∘ h и f с предобразами по h.
LaTeX
$$$ContMDiffOn I' J m (h \\circ f) s \\iff ContMDiffOn I' I m f s$$$
Lean4
@[simp]
theorem contMDiffWithinAt_diffeomorph_comp_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : M' → M} (hm : m ≤ n) {s x} :
ContMDiffWithinAt I' J m (h ∘ f) s x ↔ ContMDiffWithinAt I' I m f s x :=
⟨fun Hhf => by
simpa only [Function.comp_def, h.symm_apply_apply] using (h.symm.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hhf,
fun Hf => (h.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hf⟩