English
If ha2 ≥ 1 and h holds for all finite sets s that ∏ i∈s f(i) ≤ a2, then the infinite tprod is ≤ a2.
Русский
Если ha2 ≥ 1 и для всех конечных множеств s верно, что ∏_{i∈s} f(i) ≤ a2, то ∏'[L] i, f i ≤ a2.
LaTeX
$$$\\forall f:\\, ι \\to α, \\forall a_2:\\, α, (1 \\le a_2) \\to (\\forall s:\\, Finset ι, \\prod i \\in s, f i \\le a_2) \\to \\prod'[L] i, f i \\le a_2$$$
Lean4
@[to_additive]
theorem tprod_le_of_prod_le' (ha₂ : 1 ≤ a₂) (h : ∀ s, ∏ i ∈ s, f i ≤ a₂) : ∏'[L] i, f i ≤ a₂ :=
by
by_cases hL : L.NeBot
· by_cases hf : Multipliable f L
· exact hf.tprod_le_of_prod_le h
· rwa [tprod_eq_one_of_not_multipliable hf]
· by_cases hf : f.mulSupport.Finite
· simpa [tprod_bot hL, finprod_eq_prod _ hf] using h _
· rwa [tprod_bot hL, finprod_of_infinite_mulSupport hf]
