prod_option — Mathlib

English

For a function f: Option α → M and finite index set, the product over all i equals f none multiplied by the product over all i of f (some i).

Русский

Для функции f: Option α → M произведение по всем индексам равно f none умноженное на произведение по всем i: f (some i).

LaTeX

$$$\\prod_{i} f(i) = f(\\mathrm{none}) \\cdot \\prod_{i} f(\\mathrm{some}\\ i)$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_option (f : Option α → M) : ∏ i, f i = f none * ∏ i, f (some i) :=
  Finset.prod_insertNone f univ

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