continuousOn_iteratedDerivWithin — Mathlib

English

On a set with unique derivatives, if f is ContDiffOn 𝕜 n f s, then for every m ≤ n, iteratedDerivWithin m f s is continuous on s.

Русский

На множестве с уникальными производными, если f ∈ ContDiffOn 𝕜 n f s, тогда для каждого m ≤ n элемент iteratedDerivWithin m f s непрерывен на s.

LaTeX

$$$ContDiffOn\ 𝕜\ n\ f\ s \Rightarrow \forall m\le n,\ ContinuousOn( iteratedDerivWithin m f s) s$$$

Lean4

/-- On a set with unique derivatives, a `C^n` function has derivatives up to `n` which are
continuous. -/
theorem continuousOn_iteratedDerivWithin {n : WithTop ℕ∞} {m : ℕ} (h : ContDiffOn 𝕜 n f s) (hmn : m ≤ n)
    (hs : UniqueDiffOn 𝕜 s) : ContinuousOn (iteratedDerivWithin m f s) s := by
  simpa only [iteratedDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_continuousOn_iff] using
    h.continuousOn_iteratedFDerivWithin hmn hs

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