English
If k < m < n and x, y, z ≠ 0, then the support has exactly three elements.
Русский
Если k < m < n и x, y, z ≠ 0, то опора полинома состоит из трёх элементов.
LaTeX
$$$$\#\operatorname{Supp}(C x X^k + C y X^m + C z X^n) = 3$$$$
Lean4
theorem card_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)) = 3 := by
rw [support_trinomial hkm hmn hx hy hz,
card_insert_of_notMem (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
card_insert_of_notMem (mt mem_singleton.mp hmn.ne), card_singleton]