mem_degreesLE — Mathlib

English

Member criterion: an element belongs to degreesLE(s) iff its degree vector is bounded by s.

Русский

Критерий принадлежности: элемент принадлежит degreesLE(s) тогда и только тогда, когда вектор степеней ограничен s.

LaTeX

$$$\\\\forall p : MvPolynomial σ R, \\\\ p \\\\in degreesLE(R,\\\\sigma, s) \\\\iff \\\\ p.degrees \\\\le s$$$

Lean4

@[simp]
theorem mem_degreesLE : p ∈ degreesLE R σ s ↔ p.degrees ≤ s :=
  Iff.rfl

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