English
If deg is a degree function from A to a semilattice with supremum, then the supremum of the degrees of a sum is bounded by the supremum of the degrees of the summands: supdeg(a+b) ≤ degb a ⊔ degb b for any a,b.
Русский
Если deg — функция степеней из A в полупорядкованное множество с верхней гранью, то максимум степеней суммы не превышает максимум степеней суммирующих: deg(a+b) ≤ deg(a) ⊔ deg(b).
LaTeX
$$$\\operatorname{Supp}(f+g)\\!\\!\\!\\!\\sup \\deg \\le \\operatorname{Supp}(f)\\!\\!\\!\\!\\sup \\deg \\; \\sqcup \\; \\operatorname{Supp}(g)\\!\\!\\!\\!\\sup \\deg$$$
Lean4
theorem sup_support_add_le : (f + g).support.sup degb ≤ f.support.sup degb ⊔ g.support.sup degb := by
classical exact (Finset.sup_mono Finsupp.support_add).trans_eq Finset.sup_union
