le_inf_support_list_prod — Mathlib

English

For a list of elements, the sum of the infima of their degree supports is bounded by the infimum of the product’s support.

Русский

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

LaTeX

$$$\\sum_i (f_i\\!\\text{support.inf deg}) ≤ (\\prod_i f_i)\\!\\text{support.inf deg}$$$

Lean4

theorem le_inf_support_list_prod (degt0 : 0 ≤ degt 0) (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (l : List R[A]) :
    (l.map fun f : R[A] => f.support.inf degt).sum ≤ l.prod.support.inf degt :=
  by
  refine OrderDual.ofDual_le_ofDual.mpr ?_
  refine sup_support_list_prod_le ?_ ?_ l
  · refine (OrderDual.ofDual_le_ofDual.mp ?_)
    exact degt0
  · refine (fun a b => OrderDual.ofDual_le_ofDual.mp ?_)
    exact degtm a b

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