toOpenPartialHomeomorph_mdifferentiable

English

If h is a n-class-diffeomorphism with n ≥ 1, then the associated OpenPartialHomeomorph is MDifferentiable.

Русский

Если h — диффеоморфизм класса n с n ≥ 1, то соответствующий OpenPartialHomeomorph является MDifferentiable.

LaTeX

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

Lean4

theorem toOpenPartialHomeomorph_mdifferentiable (h : M ≃ₘ^n⟮I, J⟯ N) (hn : 1 ≤ n) :
    h.toHomeomorph.toOpenPartialHomeomorph.MDifferentiable I J :=
  ⟨h.mdifferentiableOn _ hn, h.symm.mdifferentiableOn _ hn⟩

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