finprod_eq_if — Mathlib

English

The finprod equals f h if p holds, otherwise equals 1, where h is a witness for p.

Русский

Если p истинно, то финпроизводство равно f h, иначе равно 1, где h — свидетель p.

LaTeX

$$$\\text{finprod}(f) = \\begin{cases} f(h), & \\text{if } h : p, \\\\ 1, & \\text{otherwise} \\end{cases}$$$

Lean4

@[to_additive]
theorem finprod_eq_if {p : Prop} [Decidable p] {x : M} : ∏ᶠ _ : p, x = if p then x else 1 :=
  finprod_eq_dif fun _ => x

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