support_binomial' — Mathlib

English

The support of C x · X^k + C y · X^m is contained in {k, m}.

Русский

Поддержка C x · X^k + C y · X^m ⊆ {k, m}.

LaTeX

$$$\operatorname{supp}(C x \cdot X^{k} + C y \cdot X^{m}) \subseteq \{k, m\}$$$

Lean4

theorem support_binomial' (k m : ℕ) (x y : R) : Polynomial.support (C x * X ^ k + C y * X ^ m) ⊆ { k, m } :=
  support_add.trans
    (union_subset ((support_C_mul_X_pow' k x).trans (singleton_subset_iff.mpr (mem_insert_self k { m })))
      ((support_C_mul_X_pow' m y).trans (singleton_subset_iff.mpr (mem_insert_of_mem (mem_singleton_self m)))))

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