bot_lt_prod — Mathlib

English

If every term is strictly above ⊥, then the product is strictly above ⊥.

Русский

Если каждый член множителя строго больше ⊥, то произведение строго больше ⊥.

LaTeX

$$$\forall i\in s,\ ⊥ < f(i)\Rightarrow ⊥ < \prod_{i\in s} f(i)$$$

Lean4

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

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