degreeOf_lt_iff — Mathlib

English

For a positive d, degreeOf i f < d iff every monomial m in the support of f satisfies m(i) < d.

Русский

Для положительного d, degreeOf i f < d тогда и только тогда, когда для каждого монома m в опоре f выполняется m(i) < d.

LaTeX

$$$\forall (d>0),\; degreeOf(i, f) < d \iff \forall m \in \operatorname{support}(f), m(i) < d$$$

Lean4

theorem degreeOf_lt_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) :
    degreeOf n f < d ↔ ∀ m : σ →₀ ℕ, m ∈ f.support → m n < d := by rwa [degreeOf_eq_sup, Finset.sup_lt_iff]

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