isLUB_hasProd — Mathlib

English

If all factors are at least 1 and f has a HasProd a, then a is the least upper bound of the set of finite products ∏_{i∈s} f(i).

Русский

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

LaTeX

$$$\\forall f:\\, ι\\to α,\\ a:\\, α,\\ (\\forall i, 1 \\le f(i))\\to \\text{HasProd } f\\ a\\ L\\to \\text{IsLUB }(\\{\\prod_{i\\in s} f(i)\\mid s \\text{ Finset } ι\\})\\ a$$$

Lean4

@[to_additive]
theorem isLUB_hasProd (h : ∀ i, 1 ≤ f i) (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_of_one_le' h) hf

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