le_tprod — Mathlib

English

If f ≤ g pointwise, then tprod f ≤ tprod 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 \\prod'[L] i, f i \\le \\prod'[L] i, g i$$$

Lean4

@[to_additive]
protected theorem le_tprod [L.NeBot] [L.LeAtTop] (hf : Multipliable f L) (i : ι) (hb : ∀ j ≠ i, 1 ≤ f j) :
    f i ≤ ∏'[L] i, f i :=
  le_hasProd hf.hasProd i hb

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