fun_neg — Mathlib

English

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

Русский

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

LaTeX

$$$\\forall i \\in u,\\ HasDerivAt(A_i, A'_i, x) \\Rightarrow HasDerivAt(\\lambda y. \\sum_{i\\in u} A_i(y), \\sum_{i\\in u} A'_i, x).$$$

Lean4

nonrec theorem fun_neg (h : HasDerivAt f f' x) : HasDerivAt (fun x ↦ -f x) (-f') x :=
  h.neg

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