derivWithin — Mathlib

English

On an open set, ∞-level contDiff is equivalent to differentiability and ∞-level contDiff of the derivative.

Русский

На открытой области бесконечная гладкость эквивалентна дифференцируемости и бесконечной гладкости производной.

LaTeX

$$$ContDiffOn\ 𝕜\ ∞ f_2\ s_2 \iff DifferentiableOn 𝕜 f_2\ s_2 \land ContDiffOn 𝕜 ∞ (deriv f_2)\ s_2$$$

Lean4

protected theorem derivWithin (hf : ContDiffOn 𝕜 n f₂ s₂) (hs : UniqueDiffOn 𝕜 s₂) (hmn : m + 1 ≤ n) :
    ContDiffOn 𝕜 m (derivWithin f₂ s₂) s₂ :=
  ((contDiffOn_succ_iff_derivWithin hs).1 (hf.of_le hmn)).2.2

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