of_succ — Mathlib

English

If a function is C^{n+1} on a set within a chart, then it is C^n on the same set within that chart.

Русский

Если функция C^{n+1} на множестве в карте, то она C^n на том же множестве в этой карте.

LaTeX

$$$ContMDiffWithinAt I I' (n+1) f s x \Rightarrow ContMDiffWithinAt I I' n f s x$$$

Lean4

theorem of_succ (h : ContMDiffWithinAt I I' (n + 1) f s x) : ContMDiffWithinAt I I' n f s x :=
  h.of_le le_self_add

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