prod_ite_mem — Mathlib

English

For Finset s and function f, ∏ i (if i ∈ s then f i else 1) = ∏ i ∈ s, f i.

Русский

Для множества s и функции f имеем: ∏_{i} (если i∈s, то f(i), иначе 1) = ∏_{i∈s} f(i).

LaTeX

$$$\\displaystyle \\prod_{i} \\bigl(\\operatorname{ite}(i \\in s)\\, f(i)\\, 1\\bigr) = \\prod_{i \\in s} f(i)$$$

Lean4

@[to_additive]
theorem prod_ite_mem (s : Finset ι) (f : ι → M) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by simp

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