le_inf_support_mul — Mathlib

English

A dual inequality to the previous one: the sum of infima of the supports is bounded by the infimum of the product’s support under the degree map.

Русский

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

LaTeX

$$$f^{\\text{support}}(\\deg)\\;+\\;g^{\\text{support}}(\\deg) \\le (f*g)^{\\text{support}}(\\deg)$$$

Lean4

theorem le_inf_support_mul {degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b)) (f g : R[A]) :
    f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt :=
  sup_support_mul_le (B := Tᵒᵈ) degtm f g

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