contMDiffOn_of_mem_maximalAtlas — Mathlib

English

The inverse of an extended chart is C^n on its image domain.

Русский

Обратная карта расширенного чарта является C^n на образе области определения.

LaTeX

$$$\mathrm{ContMDiffOn}\, (e.extend I)^{-1} : I'' \to e.target$$$

Lean4

/-- An atlas member is `C^n` for any `n`. -/
theorem contMDiffOn_of_mem_maximalAtlas (h : e ∈ maximalAtlas I n M) : ContMDiffOn I I n e e.source :=
  (contDiffWithinAt_localInvariantProp n).liftPropOn_of_mem_maximalAtlas contDiffWithinAtProp_id h

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