contMDiff

Mathlib.Geometry.Manifold.LocalDiffeomorph

URI: https://scilib.ai/kg/mathlib#IsLocalDiffeomorph.contMDiff

English

A C^n local diffeomorphism is C^n differentiable (the global statement).

Русский

Локальный диффеоморфизм класса C^n — это дифференцируемый отображение класса C^n.

LaTeX

$$$ IsLocalDiffeomorph I J n f \to ContMDiff I J n f $$$

Lean4

/-- A `C^n` local diffeomorphism is `C^n`. -/
theorem contMDiff (hf : IsLocalDiffeomorph I J n f) : ContMDiff I J n f := fun x ↦ (hf x).contMDiffAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru