degreeOf_le_iff — Mathlib

English

DegreeOf n f ≤ d iff every monomial in the support satisfies m(n) ≤ d.

Русский

DegreeOf n f ≤ d эквивалентно тому, что для всех мономов в опоре выполняется m(n) ≤ d.

LaTeX

$$$\operatorname{degreeOf}(n, f) \le d \iff \forall m \in \operatorname{support}(f), m(n) \le d$$$

Lean4

theorem degreeOf_le_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} : degreeOf n f ≤ d ↔ ∀ m ∈ support f, m n ≤ d := by
  rw [degreeOf_eq_sup, Finset.sup_le_iff]

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