sub — Mathlib

English

If f and g are C^n at x, then f − g is C^n at x.

Русский

Если f(x) и g(x) имеют гладкость C^n в точке x, то f(x) − g(x) тоже имеет гладкость C^n в этой точке.

LaTeX

$$ContDiffAt 𝕜 n f x \land ContDiffAt 𝕜 n g x \Rightarrow ContDiffAt 𝕜 n (f - g) x$$

Lean4

/-- The difference of two `C^n` functions at a point is `C^n` at this point. -/
@[fun_prop]
theorem sub {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) : ContDiffAt 𝕜 n (fun x => f x - g x) x :=
  by simpa only [sub_eq_add_neg] using hf.add hg.neg

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