prod_dite_eq' — Mathlib

English

For a finite set s and a fixed a, the product of (if a = x then b(x,h) else 1) over x ∈ s equals b(a) if a ∈ s, otherwise 1.

Русский

Для фиксированного a произведение (если a = x, тогда b(x,h), иначе 1) по x∈s равно b(a) если a∈s, иначе 1.

LaTeX

$$$\\prod_{x \\in s} (\\text{if } h : a = x \\text{ then } b(x,h) \\text{ else } 1) = \\text{ite}(a \\in s) (b(a, rfl)) 1.$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_dite_eq' [DecidableEq ι] (s : Finset ι) (a : ι) (b : ∀ x : ι, x = a → M) :
    ∏ x ∈ s, (if h : x = a then b x h else 1) = ite (a ∈ s) (b a rfl) 1 :=
  by
  split_ifs with h
  · rw [Finset.prod_eq_single a, dif_pos rfl]
    · intro _ _ h
      rw [dif_neg]
      exact h
    · simp [h]
  · rw [Finset.prod_eq_one]
    grind

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