toPartialDiffeomorph — Mathlib

English

A partial diffeomorphism is C^n on its domain for any n ≥ 1.

Русский

Частый диффеоморфизм дифференцируем по С^n на своей области определения для любого n ≥ 1.

LaTeX

$$MDifferentiableOn I J n Φ Φ.source$$

Lean4

/-- A diffeomorphism is a partial diffeomorphism. -/
def toPartialDiffeomorph (h : Diffeomorph I J M N n) : PartialDiffeomorph I J M N n
    where
  toPartialEquiv := h.toHomeomorph.toPartialEquiv
  open_source := isOpen_univ
  open_target := isOpen_univ
  contMDiffOn_toFun x _ := h.contMDiff_toFun x
  contMDiffOn_invFun _ _ := h.symm.contMDiffWithinAt

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