contMDiffAt_diffeomorph_comp_iff — Mathlib

English

If h is a n-class diffeomorphism, then f ∘ h is ContMDiff if and only if f is ContMDiff (with appropriate coordinates).

Русский

Если h — диффеоморфизм класса n, то f ∘ h гладко (контMDiff) тогда и только тогда, когда f гладко (с учётом соответствующих координат).

LaTeX

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

Lean4

@[simp]
theorem contMDiffAt_diffeomorph_comp_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : M' → M} (hm : m ≤ n) {x} :
    ContMDiffAt I' J m (h ∘ f) x ↔ ContMDiffAt I' I m f x :=
  h.contMDiffWithinAt_diffeomorph_comp_iff hm

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