iteratedFDeriv_const_of_ne — Mathlib

English

For any nonzero n, iteratedFDerivWithin 𝕜 n (const function) is zero.

Русский

Для любого ненулевого n итеративная производная константы внутри множества равна нулю.

LaTeX

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

Lean4

theorem iteratedFDeriv_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) : (iteratedFDeriv 𝕜 n fun _ : E ↦ c) = 0 := by
  simp only [← iteratedFDerivWithin_univ, iteratedFDerivWithin_const_of_ne hn]

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