supp_subset_range_natDegree_succ — Mathlib

English

For any polynomial p, its support is contained in the range of natDegree(p) plus one: supp(p) ⊆ range(natDegree(p) + 1).

Русский

Для любого полинома p множество степеней встречается в диапазоне от 0 до natDegree(p) включительно: supp(p) ⊆ range(natDegree(p) + 1).

LaTeX

$$$\operatorname{supp}(p) \subseteq \operatorname{range}(\operatorname{natDegree}(p) + 1).$$$

Lean4

theorem supp_subset_range_natDegree_succ : p.support ⊆ Finset.range (natDegree p + 1) :=
  supp_subset_range (Nat.lt_succ_self _)

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