English
The support has size two iff there exist k < m and nonzero x, y such that f = C x X^k + C y X^m.
Русский
Опора имеет размер два тогда и только тогда, когда существуют k < m и ненулевые x, y такие, что f = C x X^k + C y X^m.
LaTeX
$$$#f.support = 2 \\iff \\exists k,m\\, (k < m) \\land \\exists x\\,\\exists y\\, (x \\neq 0) \\land (y \\neq 0) \\,\\land f = C x X^k + C y X^m$$$
Lean4
theorem card_support_eq_two :
#f.support = 2 ↔ ∃ (k m : ℕ) (_ : k < m) (x y : R) (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m :=
by
refine ⟨fun h => ?_, ?_⟩
· obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
refine ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩
rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]
rfl
· rintro ⟨k, m, hkm, x, y, hx, hy, rfl⟩
exact card_support_binomial hkm.ne hx hy
