prod_of_isEmpty — Mathlib

English

Let I be an empty type. For every Finset s of I and every function f: I → M, the finite product ∏_{i ∈ s} f(i) equals 1.

Русский

Пусть I пустого типа. Для любого конечного множества s ⊆ I и любой функции f: I → M произведение ∏_{i ∈ s} f(i) равно 1.

LaTeX

$$$\\forall I\\; [\\text{IsEmpty }I]\\; \\forall s:\\mathrm{Finset}\\,I\\; \\forall f:I \\to M,\\; \\prod_{i \\in s} f(i) = 1$$$

Lean4

@[to_additive]
theorem prod_of_isEmpty [IsEmpty ι] (s : Finset ι) : ∏ i ∈ s, f i = 1 := by rw [eq_empty_of_isEmpty s, prod_empty]

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