supDegree_sub_le — Mathlib

English

If a support point a is a maximum with respect to the degree function D on the support of p, then the supremum degree of p equals D a.

Русский

Если точка a поддержки является максимумом по функции степеней D на поддержке p, то верхняя граница степени p равна D(a).

LaTeX

$$$\\text{If } a\\in p\\text{ supp and } IsMaxOn(D, p^{\\text{supp}}, a)\\text{ then } p^{\\sup}(D)=D(a)$$$

Lean4

theorem supDegree_sub_le {f g : R'[A]} : (f - g).supDegree D ≤ f.supDegree D ⊔ g.supDegree D := by
  rw [sub_eq_add_neg, ← supDegree_neg (f := g)]; apply supDegree_add_le

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