toOpenPartialHomeomorph — Mathlib

English

A partial diffeomorphism is C^n with continuous derivatives on its source.

Русский

Частичный диффеоморфизм имеет непрерывные производные на своей области определения.

LaTeX

$$ContMDiffOn I J n Φ Φ.source$$

Lean4

/-- A partial diffeomorphism is also a local homeomorphism. -/
def toOpenPartialHomeomorph : OpenPartialHomeomorph M N
    where
  toPartialEquiv := Φ.toPartialEquiv
  open_source := Φ.open_source
  open_target := Φ.open_target
  continuousOn_toFun := Φ.contMDiffOn_toFun.continuousOn
  continuousOn_invFun := Φ.contMDiffOn_invFun.continuousOn

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