English
The support of C x · X^k + C y · X^m + C z · X^n is contained in {k, m, n}.
Русский
Поддержка C x · X^k + C y · X^m + C z · X^n ⊆ {k, m, n}.
LaTeX
$$$\operatorname{supp}(C x \cdot X^{k} + C y \cdot X^{m} + C z \cdot X^{n}) \subseteq \{k, m, n\}$$$
Lean4
theorem support_trinomial' (k m n : ℕ) (x y z : R) :
Polynomial.support (C x * X ^ k + C y * X ^ m + C z * X ^ n) ⊆ { k, m, n } :=
support_add.trans
(union_subset
(support_add.trans
(union_subset ((support_C_mul_X_pow' k x).trans (singleton_subset_iff.mpr (mem_insert_self k { m, n })))
((support_C_mul_X_pow' m y).trans (singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_self m { n }))))))
((support_C_mul_X_pow' n z).trans
(singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n))))))
