add — Mathlib

English

Let f and g be C-polynomials at x. Then their sum f + g is also 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 add (hf : CPolynomialAt 𝕜 f x) (hg : CPolynomialAt 𝕜 g x) : CPolynomialAt 𝕜 (f + g) x :=
  let ⟨_, _, hpf⟩ := hf
  let ⟨_, _, hqf⟩ := hg
  (hpf.add hqf).cpolynomialAt

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