contMDiffOn_symm_of_mem_maximalAtlas

English

Symbolic expression of the extend-symm compatibility in smoothness classes.

Русский

Символическое выражение совместимости extend-symm в классах гладкости.

LaTeX

$$$(\text{ExtendSymm})$$$

Lean4

/-- The inverse of an atlas member is `C^n` for any `n`. -/
theorem contMDiffOn_symm_of_mem_maximalAtlas (h : e ∈ maximalAtlas I n M) : ContMDiffOn I I n e.symm e.target :=
  (contDiffWithinAt_localInvariantProp n).liftPropOn_symm_of_mem_maximalAtlas contDiffWithinAtProp_id h

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