prod_ne_bot — Mathlib

English

If every term in a finite product is non-bottom, then the product is non-bottom.

Русский

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

LaTeX

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

Lean4

/-- A product of finite terms is finite. -/
theorem prod_ne_bot (h : ∀ i ∈ s, f i ≠ ⊥) : ∏ i ∈ s, f i ≠ ⊥ :=
  prod_induction f (· ≠ ⊥) (fun _ _ ↦ mul_ne_bot) coe_ne_bot h

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