fderiv_const_add — Mathlib

English

If for all i ∈ u, HasFDerivAt (A_i) (A'_i) x, then HasFDerivAt (∑ i∈u A_i) (∑ i∈u A'_i) x.

Русский

Если для всех i∈u функция A_i имеет производную HasFDerivAt с производной A'_i в точке x, то сумма ∑ i∈u A_i имеет производную ∑ i∈u A'_i в точке x.

LaTeX

$$$\operatorname{HasFDerivAt}_{\mathbb{k}}\left(\sum_{i\in u} A_i\right)\left(\sum_{i\in u} A'_i\right)\ x$$

Lean4

@[simp]
theorem fderiv_const_add (c : F) : fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x := by
  simp only [add_comm c, fderiv_add_const]

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