prod_attach_eq_prod_dite — Mathlib

English

Relates the product over an attached Finset to a universal product with a conditional depending on membership, bridging Finset.attach and the universal representation.

Русский

Связывает произведение по присоединённому Finset с всеобщим произведением с условием по принадлежности, переходя к представлению через Finset.attach.

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]
theorem prod_attach_eq_prod_dite [Fintype ι] (s : Finset ι) (f : s → M) [DecidablePred (· ∈ s)] :
    ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1 :=
  by
  rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]
  congr
  · simp
  · ext; simp
  · apply Function.hfunext <;> simp +contextual [Subtype.heq_iff_coe_eq]

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