contMDiffAt — Mathlib

English

A local diffeomorphism at x is differentiable at x in the MDifferentiable sense, with the appropriate level.

Русский

Локальный диффеоморфизм в точке x гладок в смысле MDifferentiableAt.

LaTeX

$$$ \text{MDifferentiableAt } J I n\ hf.localInverse.toFun (f x) $$$

Lean4

/-- A `C^n` local diffeomorphism at `x` is `C^n` differentiable at `x`. -/
theorem contMDiffAt (hf : IsLocalDiffeomorphAt I J n f x) : ContMDiffAt I J n f x :=
  by
  choose Φ hx heq using hf
  exact ((Φ.contMDiffOn_toFun).congr heq).contMDiffAt (Φ.open_source.mem_nhds hx)

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