degree_add_le — Mathlib

English

The degree of the sum is bounded above by the supremum of the degrees: deg(f+g) ≤ deg f ⊔ deg g.

Русский

Степень суммы ограничена сверху супремюмом степеней: deg(f+g) ≤ deg f ⊔ deg g.

LaTeX

$$$\deg_m(f+g) \preceq_m (\deg_m f) \sqcup (\deg_m g)$$$

Lean4

theorem degree_add_le {f g : MvPolynomial σ R} :
    m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g) :=
  by
  conv_rhs => rw [← m.toSyn.apply_symm_apply (_ ⊔ _)]
  rw [degree_le_iff]
  simp only [AddEquiv.apply_symm_apply, le_sup_iff]
  intro b hb
  by_cases hf : b ∈ f.support
  · left
    exact m.le_degree hf
  · right
    apply m.le_degree
    simp only [notMem_support_iff] at hf
    simpa only [mem_support_iff, coeff_add, hf, zero_add] using hb

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