continuousOn_derivWithin — Mathlib

English

Iterating the deriv operator preserves ContDiff under appropriate hypotheses.

Русский

Повторение оператора дифференцирования сохраняет ContDiff при подходящих предположениях.

LaTeX

$$$ContDiff\ 𝕜\ (WithTop.some instTopENat.top) f_2 \Rightarrow ContDiff\ 𝕜\ (WithTop.some instTopENat.top) (Nat.iterate deriv\ n\ f_2)$$$

Lean4

theorem continuousOn_derivWithin (h : ContDiffOn 𝕜 n f₂ s₂) (hs : UniqueDiffOn 𝕜 s₂) (hn : 1 ≤ n) :
    ContinuousOn (derivWithin f₂ s₂) s₂ :=
  by
  rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl] at hn
  exact ((contDiffOn_succ_iff_derivWithin hs).1 (h.of_le hn)).2.2.continuousOn

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