supp_subset_range — Mathlib

English

If natDegree(p) < m, then every exponent appearing in p is less than m; i.e., the support of p is contained in range(m).

Русский

Если natDegree(p) < m, то каждая встречающаяся степень в p меньше m; то есть supp(p) ⊆ range(m).

LaTeX

$$$\operatorname{natDegree}(p) < m \Rightarrow \operatorname{supp}(p) \subseteq \operatorname{range}(m).$$$

Lean4

theorem supp_subset_range (h : natDegree p < m) : p.support ⊆ Finset.range m := fun _n hn =>
  mem_range.2 <| (le_natDegree_of_mem_supp _ hn).trans_lt h

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