le_infDegree_add — Mathlib

English

The infDegree of the sum dominates the infimum of the infDegrees of the summands: infDegree(f) ∧ infDegree(g) ≤ infDegree(f+g).

Русский

Наименьшая степень суммой не меньше, чем наименьшая степень каждого слагаемого; выступает нестрогое неравенство.

LaTeX

$$$$\operatorname{infDegree}_D(f) \wedge \operatorname{infDegree}_D(g) \le \operatorname{infDegree}_D(f+g).$$$$

Lean4

theorem le_infDegree_add (f g : R[A]) : (f.infDegree D) ⊓ (g.infDegree D) ≤ (f + g).infDegree D :=
  le_inf_support_add D f g

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