prod_le_tprod — Mathlib

English

For a finite set s, the finite product of f on s is bounded above by the infinite product tprod of f with respect to the same filter L.

Русский

Для конечного множества s произведение f на s не превосходит бесконечного произведения tprod f по тому же фильтру.

LaTeX

$$$\\forall s:\\, Finset\\ ι, (s.prod (fun i => f i)) \\le \\prod'[L] i, f i$$$

Lean4

@[to_additive]
protected theorem prod_le_tprod [L.NeBot] [L.LeAtTop] {f : ι → α} (s : Finset ι) (hs : ∀ i, i ∉ s → 1 ≤ f i)
    (hf : Multipliable f L) : ∏ i ∈ s, f i ≤ ∏'[L] i, f i :=
  prod_le_hasProd s hs hf.hasProd

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