contMDiff_tangentMap — Mathlib

English

If a function is C^n, then its tangent map is C^m.

Русский

Если функция C^n, то касательное отображение tangentMap тоже C^m.

LaTeX

$$$\forall hf : ContMDiff I I' n f,\; hmn : m + 1 ≤ n \Rightarrow ContMDiff I.tangent I'.tangent m (tangentMap I I' f)$$$

Lean4

/-- If a function is `C^n`, then its bundled derivative is `C^m` when `m+1 ≤ n`. -/
theorem contMDiff_tangentMap (hf : ContMDiff I I' n f) (hmn : m + 1 ≤ n) :
    ContMDiff I.tangent I'.tangent m (tangentMap I I' f) :=
  by
  rw [← contMDiffOn_univ] at hf ⊢
  convert hf.contMDiffOn_tangentMapWithin hmn uniqueMDiffOn_univ
  rw [tangentMapWithin_univ]

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