fun_add — Mathlib

English

Let f and g be differentiable within s at x with derivatives f' and g'. Then the derivative within s of f + g at x is f' + g'.

Русский

Пусть f и g дифференцируемы в рамках множества s в точке x с производными f' и g'. Тогда производная внутри s от f + g в x равна f' + g'.

LaTeX

$$$HasDerivWithinAt f f' s x \land HasDerivWithinAt g g' s x \Rightarrow HasDerivWithinAt (f + g) (f' + g') s x$$$

Lean4

nonrec theorem fun_add (hf : HasDerivWithinAt f f' s x) (hg : HasDerivWithinAt g g' s x) :
    HasDerivWithinAt (fun y ↦ f y + g y) (f' + g') s x :=
  hf.add hg

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