prod_ne_top — Mathlib

English

Let s be a finite set and f: α → ℝ≥0∞. If each f(a) ≠ ∞ for a ∈ s, then the product ∏_{a∈s} f(a) ≠ ∞.

Русский

Пусть s—конечное множество и x: α → ℝ≥0∞. Если для каждого a ∈ s значение f(a) не равно бесконечности, то произведение по a∈s f(a) не равно бесконечности.

LaTeX

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

Lean4

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

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