tprod_strict_mono — Mathlib

English

If f and g are comparable and f < g, then tprod f < tprod g.

Русский

Если f и g сравнимы и f < g, то tprod f < tprod g.

LaTeX

$$$\\forall f,g:\\, \\text{Multipliable } f L \\to \\text{Multipliable } g L \\to \\text{Pi.preorder.lt } f g \\to \\text{tprod } f L < \\text{tprod } g L$$$

Lean4

@[to_additive (attr := mono)]
protected theorem tprod_strict_mono [L.NeBot] [L.LeAtTop] (hf : Multipliable f L) (hg : Multipliable g L) (h : f < g) :
    ∏'[L] n, f n < ∏'[L] n, g n :=
  let ⟨hle, _i, hi⟩ := Pi.lt_def.mp h
  hf.tprod_lt_tprod hle hi hg

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