isLocalDiffeomorphOn

Mathlib.Geometry.Manifold.LocalDiffeomorph

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

English

If x is the point of local diffeomorphism for f, then f is C^n-differentiable at x.

Русский

Если x — точка локального диффеоморфизма f, то f гладко дифференцируема класса C^n в точке x.

LaTeX

$$$ ContMDiffAt I J n f x $$$

Lean4

theorem isLocalDiffeomorphOn {f : M → N} (hf : IsLocalDiffeomorph I J n f) (s : Set M) :
    IsLocalDiffeomorphOn I J n f s := fun x ↦ hf x

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

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

Разделы

Аффилиация

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