degree_add_le_of_le — Mathlib

English

If deg p ≤ a and deg q ≤ b, then deg(p+q) ≤ max(a,b).

Русский

Если deg p ≤ a и deg q ≤ b, то deg(p+q) ≤ max(a,b).

LaTeX

$$$ \operatorname{degree}(p+q) \le \max(a, b) \text{ при } \operatorname{degree}(p) \le a \text{ и } \operatorname{degree}(q) \le b $$$

Lean4

theorem degree_add_le_of_le {a b : WithBot ℕ} (hp : degree p ≤ a) (hq : degree q ≤ b) : degree (p + q) ≤ max a b :=
  (p.degree_add_le q).trans <| max_le_max ‹_› ‹_›

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