finprod_eq_dif — Mathlib

English

A definitional equality for finprod: finprod f equals the delta-form decomposition stated earlier.

Русский

Определительная равенство для finprod: итог равен разложению в форму delta как выше.

LaTeX

$$$\\mathrm{finprod}(f) = \\big(\\text{if }\\cdots\\text{ then }\\cdots \\text{ else } 1\\big)$$$

Lean4

@[to_additive]
theorem finprod_eq_dif {p : Prop} [Decidable p] (f : p → M) : ∏ᶠ i, f i = if h : p then f h else 1 :=
  by
  split_ifs with h
  · haveI : Unique p := ⟨⟨h⟩, fun _ => rfl⟩
    exact finprod_unique f
  · haveI : IsEmpty p := ⟨h⟩
    exact finprod_of_isEmpty f

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