iteratedFDerivWithin_const_of_ne — Mathlib

English

If n > 0 and f is a constant function f(x) = c, then its nth iterated derivative within any set s is zero.

Русский

Если n > 0 и f константна, то ее n-я итерационная производная внутри любой области s равна нулю.

LaTeX

$$$ n \neq 0 \Rightarrow \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{n}(\lambda x. c)(s) = 0 $$$

Lean4

theorem iteratedFDerivWithin_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) (s : Set E) :
    iteratedFDerivWithin 𝕜 n (fun _ : E ↦ c) s = 0 := by
  cases n with
  | zero => contradiction
  | succ n => exact iteratedFDerivWithin_succ_const n c

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