hasProd_of_isLUB_of_one_le — Mathlib

English

Let f: ι → α. If every f(i) ≥ 1 and i is an upper bound of the finite partial products, then HasProd f i holds.

Русский

Пусть f: ι → α; если f(i) ≥ 1 для всех i и i является верхней гранью конечных частичных произведений, тогда HasProd f i выполняется.

LaTeX

$$IsLUB (Set.range fun s => s.prod fun i => f i) i \\Rightarrow HasProd f i$$

Lean4

@[to_additive]
theorem hasProd_of_isLUB_of_one_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] [TopologicalSpace α]
    [OrderTopology α] {f : ι → α} (i : α) (h : ∀ i, 1 ≤ f i) (hf : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) i) :
    HasProd f i :=
  tendsto_atTop_isLUB (Finset.prod_mono_set_of_one_le' h) hf

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