mdifferentiable — Mathlib

English

A local diffeomorphism at x is differentiable at x for level n with n ≥ 1.

Русский

Локальный диффеоморфизм в точке x гладок в точке x на уровне n при n ≥ 1.

LaTeX

$$$ \forall x, \; IsLocalDiffeomorphAt I J n f x \to 1 \le n \to MDifferentiableAt I J f x $$$

Lean4

/-- A `C^n` local diffeomorphism is differentiable. -/
theorem mdifferentiable (hf : IsLocalDiffeomorph I J n f) (hn : 1 ≤ n) : MDifferentiable I J f := fun x ↦
  (hf x).mdifferentiableAt hn

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