one_le_tprod — Mathlib

English

If g has some index with g i > 1 and all other entries are at least 1, then the tprod over g is strictly greater than 1.

Русский

Если есть индекс i, такой что g(i) > 1 и все остальные ≥ 1, то tprod g > 1.

LaTeX

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

Lean4

@[to_additive tsum_nonneg]
theorem one_le_tprod (h : ∀ i, 1 ≤ g i) : 1 ≤ ∏'[L] i, g i :=
  by
  by_cases hg : Multipliable g L
  · by_cases hL : L.NeBot
    · exact hg.hasProd.one_le h
    · simpa [tprod_bot hL] using one_le_finprod' h
  · rw [tprod_eq_one_of_not_multipliable hg]

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