prod_coe_sort — Mathlib

English

For a finite set s of indices ι and a function f : ι → M, the product over the elements i of s considered as a Finite Set equals the product over i ∈ s of f i: ∏ i : s, f i = ∏ i ∈ s, f i.

Русский

Для конечного множества s индексов ι и функции f: ι → M произведение по элементам i из s как по элементам множества равно произведению по i ∈ s: ∏ i : s, f i = ∏ i ∈ s, f i.

LaTeX

$$$\displaystyle \prod i : s\, f i = \prod i \in s, f i$$$

Lean4

@[to_additive]
theorem prod_coe_sort : ∏ i : s, f i = ∏ i ∈ s, f i :=
  prod_attach _ _

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