prod_dite_eq — Mathlib

English

A refinement of the previous equality with a stronger form of the attachment equivalence, mapping between attached indices and their base.

Русский

Уточнение предыдущего равенства с более сильной формой соответствия присоединения индексов и их основы.

LaTeX

$$$\\prod_{i \\in s.attach} f(i) = \\prod_{i} \\text{if } i \\in s \\text{ then } f(i) \\text{ else } 1.$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_dite_eq [DecidableEq ι] (s : Finset ι) (a : ι) (b : ∀ x : ι, a = x → M) :
    ∏ x ∈ s, (if h : a = x 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.symm
    · simp [h]
  · rw [Finset.prod_eq_one]
    grind

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