uniqueMDiffOn_image_aux — Mathlib

English

Same as above: the induced OpenPartialHomeomorph from a C^n-diffeomorphism with n ≥ 1 is MDifferentiable.

Русский

То же самое: индуцированный OpenPartialHomeomorph от C^n-диффеоморфизма с n ≥ 1 является MDifferentiable.

LaTeX

$$h.toHomeomorph.toOpenPartialHomeomorph.MDifferentiable I J$$

Lean4

theorem uniqueMDiffOn_image_aux (h : M ≃ₘ^n⟮I, J⟯ N) (hn : 1 ≤ n) {s : Set M} (hs : UniqueMDiffOn I s) :
    UniqueMDiffOn J (h '' s) :=
  by
  convert hs.uniqueMDiffOn_preimage (h.toOpenPartialHomeomorph_mdifferentiable hn)
  simp [h.image_eq_preimage]

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