differentiableOn — Mathlib

English

If h := ContDiffOn 𝕜 1 f s, then f is differentiable on s; i.e., DifferentiableOn 𝕜 f s.

Русский

Если f ∈ ContDiffOn 𝕜 1 f s, то f дифференцируема на s; т.е. DifferentiableOn 𝕜 f s.

LaTeX

$$$ContDiffOn\\ 𝕜\\ 1\\ f\\ s\\rightarrow DifferentiableOn\\ 𝕜\\ f\\ s$$$

Lean4

/-- If a function is `C^n` on a set with `n ≥ 1`, then it is differentiable there. -/
theorem differentiableOn (h : ContDiffOn 𝕜 n f s) (hn : 1 ≤ n) : DifferentiableOn 𝕜 f s := fun x hx =>
  (h x hx).differentiableWithinAt hn

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