fun_sub — Mathlib

English

If f and g are differentiable on a set s, then the difference y ↦ f(y) − g(y) is differentiable on s.

Русский

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

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{k}}(f,s) \\land \\text{DifferentiableOn}_{\\mathbb{k}}(g,s) \\Rightarrow \\text{DifferentiableOn}_{\\mathbb{k}}(\\lambda y. f(y) - g(y), s)$$$

Lean4

@[fun_prop]
theorem fun_sub (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y - g y) s := fun x hx => (hf x hx).sub (hg x hx)

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