finprod_set_coe_eq_finprod_mem — Mathlib

English

For any set s, the finprod over the elements of s as a subtype equals the finprod over s with membership indexing: ∏ᶠ j: s, f j = ∏ᶠ i ∈ s, f i.

Русский

Для множества s произведение по элементам суженного множества равно произведению по элементам s: ∏ᶠ j: s, f j = ∏ᶠ i ∈ s, f i.

LaTeX

$$$\\prod^\\!f j : s, f(j) = \\prod^\\!f i \\in s, f(i)$$$

Lean4

@[to_additive]
theorem finprod_set_coe_eq_finprod_mem (s : Set α) : ∏ᶠ j : s, f j = ∏ᶠ i ∈ s, f i :=
  by
  rw [← finprod_mem_range, Subtype.range_coe]
  exact Subtype.coe_injective

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