contMDiffOn_comp_diffeomorph_iff — Mathlib

English

For h a suitable diffeomorphism, contMDiff at of h ∘ f at x is equivalent to contMDiff at of f at x with adjusted coordinates.

Русский

Для подходящего диффеоморфизма h свойство contMDiffAt для h ∘ f в точке x эквивалентно contMDiffAt для f в той же точке, с изменёнными координатами.

LaTeX

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

Lean4

@[simp]
theorem contMDiffOn_comp_diffeomorph_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : N → M'} {s} (hm : m ≤ n) :
    ContMDiffOn I I' m (f ∘ h) s ↔ ContMDiffOn J I' m f (h.symm ⁻¹' s) :=
  h.toEquiv.forall_congr fun {_} => by
    simp only [hm, coe_toEquiv, h.symm_apply_apply, contMDiffWithinAt_comp_diffeomorph_iff, mem_preimage]

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