finprod_mem_empty — Mathlib

English

The product over an empty set is the unit: for any f, ∏_{i ∈ ∅} f(i) = 1.

Русский

Произведение по пустому множеству равно единице: для любой функции f, \prod_{i \in \emptyset} f(i) = 1.

LaTeX

$$\prod_{i \in \emptyset} f(i) = 1$$

Lean4

/-- The product of any function over an empty set is `1`. -/
@[to_additive /-- The sum of any function over an empty set is `0`. -/
    ]
theorem finprod_mem_empty : (∏ᶠ i ∈ (∅ : Set α), f i) = 1 := by simp

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