sub — Mathlib

English

If f and g are C-polynomials on s, then f - g is a C-polynomial on s.

Русский

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

LaTeX

$$CPolynomialOn 𝕜 f s \land CPolynomialOn 𝕜 g s \Rightarrow CPolynomialOn 𝕜 (f - g) s$$

Lean4

theorem sub {s : Set E} (hf : CPolynomialOn 𝕜 f s) (hg : CPolynomialOn 𝕜 g s) : CPolynomialOn 𝕜 (f - g) s := fun z hz =>
  (hf z hz).sub (hg z hz)

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