tprod_lt_tprod — Mathlib

English

If f ≤ g and f i < g i for some i, then tprod f < tprod g.

Русский

Если f ≤ g и существует i с f i < g i, то tprod f < tprod g.

LaTeX

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

Lean4

@[to_additive]
protected theorem tprod_lt_tprod [L.NeBot] [L.LeAtTop] (h : f ≤ g) (hi : f i < g i) (hf : Multipliable f L)
    (hg : Multipliable g L) : ∏'[L] n, f n < ∏'[L] n, g n :=
  hasProd_lt h hi hf.hasProd hg.hasProd

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