fderivWithin_const_add — Mathlib

English

If each A_i has a strict derivative A'_i at x, then the finite sum ∑ i∈u A_i has derivative ∑ i∈u A'_i at x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem fderivWithin_const_add (c : F) : fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x := by
  simpa only [add_comm] using fderivWithin_add_const c

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