card_roots_toFinset_le_derivative

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) _

Похожие утверждения