prod_set_coe — Mathlib

English

For a set s ⊆ ι with Finite type, and a function f : ι → M, the product over s as a set equals the product over s.toFinset: ∏ i ∈ s, f i = ∏ i ∈ s.toFinset, f i.

Русский

Для множества s ⊆ ι с конечным числом элементов произведение по элементам множества равно произведению по элементам множества-окружности: ∏ i ∈ s, f i = ∏ i ∈ s.toFinset, f i.

LaTeX

$$$\displaystyle \prod i \in s, f i = \prod i \in s.toFinset, f i$$$

Lean4

@[to_additive]
theorem prod_set_coe (s : Set ι) [Fintype s] : (∏ i : s, f i) = ∏ i ∈ s.toFinset, f i :=
  (Finset.prod_subtype s.toFinset (fun _ ↦ Set.mem_toFinset) f).symm

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