le_hasProd_of_le_prod — Mathlib

English

If for every finite set s, the product ∏_{i∈s} f(i) ≤ c, then the bilateral product a of f is ≤ c.

Русский

Если для каждого конечного множества s произведение ∏_{i∈s} f(i) ≤ c, то двустороннее произведение a ≤ c.

LaTeX

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

Lean4

@[to_additive]
theorem le_hasProd_of_le_prod [ClosedIciTopology α] [L.NeBot] (hf : HasProd f a L) (h : ∀ s, c ≤ ∏ i ∈ s, f i) :
    c ≤ a :=
  ge_of_tendsto' hf h

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