prod_lt_top — Mathlib

English

If a finite family of elements in WithTop M₀ are all finite (i.e., strictly below ⊤), then their finite product is also finite (below ⊤).

Русский

Если у конечного набора индексов s и функции f: s → WithTop M₀ все значения строго меньше ⊤, то их произведение по i ∈ s также меньше ⊤.

LaTeX

$$$\forall s:\ Finset\ ι,\ ∀ f:\ ι \to WithTop\ M_0,\big(\forall i\in s,\ f(i) < \top\big)\Rightarrow \prod_{i\in s} f(i) < \top$$$

Lean4

/-- A product of finite terms is finite. -/
theorem prod_lt_top [LT M₀] (h : ∀ i ∈ s, f i < ⊤) : ∏ i ∈ s, f i < ⊤ :=
  prod_induction f (· < ⊤) (fun _ _ ↦ mul_lt_top) (coe_lt_top _) h

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