contMDiff_diffeomorph_comp_iff — Mathlib

English

If h is a suitable n-diffeomorphism, then for any f, ContMDiff I' J m (h ∘ f) ↔ ContMDiff I' I m f.

Русский

Если h — подходящий диффеоморфизм класса n, то ContMDiff I' J m (h ∘ f) эквивалентно ContMDiff I' I m f.

LaTeX

$$$ContMDiff I' J m (h \\circ f) \\iff ContMDiff I' I m f$$$

Lean4

@[simp]
theorem contMDiff_diffeomorph_comp_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : M' → M} (hm : m ≤ n) :
    ContMDiff I' J m (h ∘ f) ↔ ContMDiff I' I m f :=
  forall_congr' fun _ => h.contMDiffWithinAt_diffeomorph_comp_iff hm

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