sub — Mathlib

English

If f and g are differentiable on a set s, then f − g is differentiable on s.

Русский

Если функции f и g дифференцируемы на s, то f − g дифференцируема на s.

LaTeX

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

Lean4

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

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