of_le — Mathlib

English

A function is C^(n+1) at x iff there exists a derivative f' with HasFDerivAt along a neighborhood and f' is C^n at x.

Русский

Функция является C^(n+1) в точке x тогда и только тогда, когда существует производная f' с HasFDerivAt в окрестности x и f' является C^n в x.

LaTeX

$$$contDiffAt_succ_iff_hasFDerivAt :\n\ ContDiffAt 𝕜 (n+1) f x \iff \exists f' : E \to E \toL[𝕜] F, (\exists u \in 𝓝 x, \forall x \in u, HasFDerivAt f (f' x) x) \wedge ContDiffAt 𝕜 n f' x$$$

Lean4

@[fun_prop]
theorem of_le (h : ContDiff 𝕜 n f) (hmn : m ≤ n) : ContDiff 𝕜 m f :=
  contDiffOn_univ.1 <| (contDiffOn_univ.2 h).of_le hmn

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