sub — Mathlib

English

If f and g are C-polynomials at x, then their difference f - g is a C-polynomial at x.

Русский

Если f и g являются C-полиномами в точке x, то разность f - g тоже является C-полином в точке x.

LaTeX

$$CPolynomialAt 𝕜 f x \land CPolynomialAt 𝕜 g x \Rightarrow CPolynomialAt 𝕜 (f - g) x$$

Lean4

theorem sub (hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) : CPolynomialAt 𝕜 (f - g) x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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