mem_restrictDegree — Mathlib

English

p belongs to restrictDegree iff every monomial in its support has per-variable exponents ≤ m.

Русский

p принадлежит restrictDegree σ R n тогда и только тогда, когда для каждого с в поддержке p выполняется s i ≤ n для всех i.

LaTeX

$$$p \\in \\mathrm{restrictDegree}(\\sigma,R,n) \\iff \\forall s \\in p.\\mathrm{support}, \\forall i, (s : \\sigma \\to \\mathbb{N}) i \\le n$$$

Lean4

theorem mem_restrictDegree (p : MvPolynomial σ R) (n : ℕ) :
    p ∈ restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ i, (s : σ →₀ ℕ) i ≤ n :=
  by
  rw [restrictDegree, restrictSupport, Finsupp.mem_supported]
  rfl

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