contMDiffWithinAt_diffeomorph_comp_iff

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⟩

Похожие утверждения