fun_add — Mathlib

English

If f and g are differentiable on s, then y ↦ f(y) + g(y) is differentiable on s.

Русский

Если f и g дифференцируемы на множестве s, то функция y ↦ f(y) + g(y) дифференцируема на s.

LaTeX

$$$\\displaystyle \\text{DifferentiableOn } 𝕜 f s \\land \\text{DifferentiableOn } 𝕜 g s \\Rightarrow \\text{DifferentiableOn } 𝕜 (f+g) s.$$$

Lean4

@[fun_prop]
theorem fun_add (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y + g y) s := fun x hx => (hf x hx).add (hg x hx)

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