degreeOf_eq_sup — Mathlib

English

DegreeOf n f equals the supremum over the support of f of the n-th coordinate: degreeOf n f = sup_{m ∈ support(f)} m(n).

Русский

DegreeOf n f равен верхней грани множества значений координаты n над опорой f: degreeOf n f = sup_{m ∈ support(f)} m(n).

LaTeX

$$$\operatorname{degreeOf}(n, f) = \operatorname{sup}_{m \in \operatorname{support}(f)} m(n)$$$

Lean4

theorem degreeOf_eq_sup (n : σ) (f : MvPolynomial σ R) : degreeOf n f = f.support.sup fun m => m n := by
  classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]

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