sub — Mathlib

English

If f and g are differentiable on s with continuous derivatives, then f − g is differentiable on s.

Русский

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

LaTeX

$$$\text{If } \text{DiffContOnCl}(\mathfrak{f}, s) \text{ and } \text{DiffContOnCl}(\mathfrak{g}, s), \text{ then } \text{DiffContOnCl}(\mathfrak{f} - \mathfrak{g}, s).$$$

Lean4

theorem sub (hf : DiffContOnCl 𝕜 f s) (hg : DiffContOnCl 𝕜 g s) : DiffContOnCl 𝕜 (f - g) s :=
  ⟨hf.1.sub hg.1, hf.2.sub hg.2⟩

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