mem_restrictDegree_iff_sup — Mathlib

English

With [DecidableEq σ], membership in restrictDegree σ R n is equivalent to suprema of counts of degrees.

Русский

При наличии [DecidableEq σ] принадлежность к restrictDegree σ R n эквивалентна сумме степеней по каждому индексу.

LaTeX

$$$p \\in \\mathrm{restrictDegree}(\\sigma,R,n) \\\\iff \\forall i, p.\\mathrm{degrees}.count i \\le n$$$

Lean4

theorem mem_restrictDegree_iff_sup [DecidableEq σ] (p : MvPolynomial σ R) (n : ℕ) :
    p ∈ restrictDegree σ R n ↔ ∀ i, p.degrees.count i ≤ n :=
  by
  simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset, Finset.sup_le_iff]
  exact ⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩

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