prod_lt_top — Mathlib

English

If every a ∈ s satisfies f(a) < ∞, then the product ∏_{a∈s} f(a) < ∞.

Русский

Если для каждого a ∈ s выполняется f(a) < ∞, то произведение ∏_{a∈s} f(a) < ∞.

LaTeX

$$$\left(\forall a \in s, f(a) < \infty\right) \Rightarrow \prod_{a\in s} f(a) < \infty$$$

Lean4

/-- A product of finite numbers is still finite. -/
theorem prod_lt_top (h : ∀ a ∈ s, f a < ∞) : ∏ a ∈ s, f a < ∞ :=
  WithTop.prod_lt_top h

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