supDegree_mul_le — Mathlib

English

If D preserves addition (D(a1 + a2) = D(a1) + D(a2)) and B is additive left- and right-mono, then the supremum degree of a product is bounded by the sum of the supremum degrees.

Русский

Если D сохраняет сложение, а B имеет монотонное сложение слева и справа, то supDegree(p q) ≤ supDegree(p) + supDegree(q).

LaTeX

$$$\left(p \ast q\right).supDegree D \le p.supDegree D + q.supDegree D$$$

Lean4

theorem supDegree_mul_le (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) [AddLeftMono B] [AddRightMono B] :
    (p * q).supDegree D ≤ p.supDegree D + q.supDegree D :=
  sup_support_mul_le (fun {_ _} => (hadd _ _).le) p q

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