support_derivativeFinsupp_subset_range

English

For p ∈ R[X] and n ∈ ℕ, if natDegree(p) < n, then the support of derivativeFinsupp(p) is contained in range n.

Русский

Для p ∈ R[X] и n ∈ ℕ, если natDegree(p) < n, то поддержка derivativeFinsupp(p) вкладывается в множество {0,1,...,n-1}.

LaTeX

$$$$ \operatorname{supp}(\mathrm{derivativeFinsupp}(p)) \subseteq \operatorname{range}(n) $$$$

Lean4

@[simp]
theorem support_derivativeFinsupp_subset_range {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
    (derivativeFinsupp p).support ⊆ range n := by
  dsimp [derivativeFinsupp]
  exact Finsupp.support_onFinset_subset.trans (Finset.range_subset_range.mpr h)

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