tprod_le_of_prod_range_le — Mathlib

English

If HasProd f a L and for all s, c ≤ ∏_{i∈s} f(i), then c ≤ a.

Русский

Если произведение HasProd f a L и для всех s выполняется c ≤ ∏_{i∈s} f(i), тогда c ≤ a.

LaTeX

$$$\\displaystyle \\text{HasProd } f\\ a\\; L \\Rightarrow (\\forall s, c \\le \\prod_{i\\in s} f(i)) \\Rightarrow c \\le a$$$

Lean4

@[to_additive]
protected theorem tprod_le_of_prod_range_le [ClosedIicTopology α] {f : ℕ → α} (hf : Multipliable f)
    (h : ∀ n, ∏ i ∈ range n, f i ≤ c) : ∏' n, f n ≤ c :=
  le_of_tendsto' hf.hasProd.tendsto_prod_nat h

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