English
For a real polynomial p, the number of real roots (distinct) is at most the number of real roots of its derivative plus one.
Русский
Для действительного многочлена p число его действительных корней (различных) не более чем число корней производной p плюс один.
LaTeX
$$$p.toFinset\text{.card} \le p'.toFinset\text{.card} + 1$$$
Lean4
/-- The number of roots of a real polynomial is at most the number of roots of its derivative plus
one. -/
theorem card_roots_toFinset_le_derivative (p : ℝ[X]) : p.roots.toFinset.card ≤ p.derivative.roots.toFinset.card + 1 :=
p.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ.trans <|
add_le_add_right (Finset.card_mono Finset.sdiff_subset) _