contMDiffOn_diffeomorph_comp_iff — Mathlib

English

For an n-class-diffeomorphism h: M → N, the ContMDiffOn of h ∘ f with respect to I' J m equals the ContMDiffOn of f with respect to I' I m.

Русский

Для диффеоморфизма класса n h: M → N выполняется эквивалентность ContMDiffOn(h ∘ f) относительно координат I',J и m и ContMDiffOn(f) относительно I',I и m.

LaTeX

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

Lean4

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

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