tprod_le_one — Mathlib

English

If all f i ≤ 1, then the tprod of f is ≤ 1.

Русский

Если все f i ≤ 1, то tprod f ≤ 1.

LaTeX

$$$\\forall f:\\, ι \\to α, (\\forall i, f i \\le 1) \\to \\text{tprod } f L \\le 1$$$

Lean4

@[to_additive]
theorem tprod_le_one (h : ∀ i, f i ≤ 1) : ∏'[L] i, f i ≤ 1 :=
  by
  by_cases hf : Multipliable f L
  · by_cases hL : L.NeBot
    · exact hf.hasProd.le_one h
    · simp only [tprod_bot hL]
      exact finprod_induction (· ≤ 1) le_rfl (fun _ _ ↦ mul_le_one') h
  · rw [tprod_eq_one_of_not_multipliable hf]

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