le_inf_support_add — Mathlib

English

For a degree function to a semilattice-inf type T, the infimum of the degrees of the coefficients of two elements satisfies an inequality comparing to the infimum in the product element.

Русский

Для функции степеней в т.л. инфимум степеней коэффициентов двух элементов удовлетворяет нестрогому неравенству по сравнению с инфимумом в произведенном элементе.

LaTeX

$$$f\\!\\!\\!\\!\\inf\\deg \\;\\;\\;\\;\\land \\;g\\!\\!\\!\\!\\inf \\deg \\le (f+g)\\!\\!\\!\\!\\inf \\deg$$$

Lean4

theorem le_inf_support_add : f.support.inf degt ⊓ g.support.inf degt ≤ (f + g).support.inf degt :=
  sup_support_add_le (fun a : A => OrderDual.toDual (degt a)) f g

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