English
Let f: Option α → M. If mulSupport (f ∘ some) is finite, then the product over o ∈ Option α equals f none times the product over a of f (some a).
Русский
Пусть f: Option α → M; если mulSupport (f ∘ some) конечно, то произведение по опциям равно f none умножить на произведение по some a: f(some a).
LaTeX
$$$\\prod^\\!o, f(o) = f(\\text{none}) \\cdot \\prod^\\!a, f({\\text{some}}\,a)$$$
Lean4
@[to_additive]
theorem finprod_option {f : Option α → M} (hf : (mulSupport (f ∘ some)).Finite) :
∏ᶠ o, f o = f none * ∏ᶠ a, f (some a) :=
by
replace hf : (mulSupport f).Finite := by simpa [finite_option]
convert finprod_mem_insert' f (show none ∉ Set.range Option.some by simp) (hf.subset inter_subset_right)
· simp
· rw [finprod_mem_range]
exact Option.some_injective _
