one_lt_tprod — Mathlib

English

If g is Multipliable and there exists i with 1 < g i, then 1 < tprod g.

Русский

Если g — Multipliable и существует i с 1 < g i, то 1 < tprod g.

LaTeX

$$$\\forall g:\\, (\\text{Multipliable } g L) \\to (\\exists i, 1 < g i) \\to 1 < \\text{tprod } g L$$$

Lean4

@[to_additive Summable.tsum_pos]
protected theorem one_lt_tprod [L.LeAtTop] [L.NeBot] (hsum : Multipliable g L) (hg : ∀ i, 1 ≤ g i) (i : ι)
    (hi : 1 < g i) : 1 < ∏'[L] i, g i := by
  rw [← tprod_one (L := L)]
  exact multipliable_one.tprod_lt_tprod hg hi hsum

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