English
Let k < m < n and x, y, z ≠ 0 in R. Then the support of C x X^k + C y X^m + C z X^n is exactly {k, m, n}.
Русский
Пусть k < m < n и x, y, z ≠ 0 в R. Тогда опора полинома C x X^k + C y X^m + C z X^n равна {k, m, n}.
LaTeX
$$$$\operatorname{Supp}(C x X^k + C y X^m + C z X^n) = \{k, m, n\}$$$$
Lean4
theorem support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
support (C x * X ^ k + C y * X ^ m + C z * X ^ n) = { k, m, n } :=
by
apply subset_antisymm (support_trinomial' k m n x y z)
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one,
coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne, if_neg hmn.ne', if_neg (hkm.trans hmn).ne,
if_neg (hkm.trans hmn).ne', mul_zero, add_zero, zero_add, Ne, hx, hy, hz, not_false_eq_true, and_true]
