isLUB_hasProd' — Mathlib

English

If HasProd f a holds, then the set of finite partial products { ∏ i ∈ s, f(i) } has a least upper bound equal to a.

Русский

Если выполнено HasProd f a, то множество конечных частичных произведений { ∏ i ∈ s, f(i) } имеет наименьшую верхнюю грань, равную a.

LaTeX

$$IsLUB (Set.range fun s => ∏ i ∈ s, f i) a$$

Lean4

@[to_additive]
theorem isLUB_hasProd' (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a := by
  classical exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

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