English
If deg is a degree function with a monotone bound under addition and f,g are in the monoid algebra, then the supremum of the degree of their product is bounded by the sum of the suprema of f and g.
Русский
Если deg — функция градусов с монотонным ограничением под сложение, и f,g принадлежат алгебре моноидов, то верхняя грань степени произведения ограничена суммой верхних граней степеней f и g.
LaTeX
$$$ (f*g)\\!\\!\\!\\!\\sup \\deg \\le f\\!\\!\\!\\!\\sup \\deg + g\\!\\!\\!\\!\\sup \\deg $$$
Lean4
theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b) (f g : R[A]) :
(f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := by
classical
exact
(Finset.sup_mono <| support_mul _ _).trans <|
Finset.sup_add_le.2 fun _fd fds _gd gds ↦ degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds)
