tprod_le_tprod — Mathlib

English

For Multipliable f and g with f ≤ g, tprod f ≤ tprod g.

Русский

Для Multipliable f и g при f ≤ g выполняется tprod f ≤ tprod g.

LaTeX

$$$\\forall f,g:\\, (\\forall i, f(i) \\le g(i)) \\to \\text{Multipliable } f L \\to \\text{Multipliable } g L \\to \\text{tprod } f L \\le \\text{tprod } g L$$$

Lean4

@[to_additive (attr := gcongr)]
protected theorem tprod_le_tprod [L.NeBot] (h : ∀ i, f i ≤ g i) (hf : Multipliable f L) (hg : Multipliable g L) :
    ∏'[L] i, f i ≤ ∏'[L] i, g i :=
  hasProd_le h hf.hasProd hg.hasProd

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