prod_finset_coe — Mathlib

English

Let p be a predicate on ι and F a finite type of the subtype {x // p x}. For a function f : ι → M, the product over the Finset s of ι when h : ∀ x, x ∈ s ↔ p x, equals the product over the subtype: ∏ a ∈ s, f a = ∏ a : Subtype p, f a.

Русский

Пусть p — предикат на ι и F — конечный тип подтипа {x | p x}. Для функции f: ι → M произведение по Finset s равно произведению по подтипу: ∏ a ∈ s, f a = ∏ a : Subtype p, f a, если h: ∀ x, x ∈ s ↔ p x.

LaTeX

$$$\displaystyle \prod a ∈ s, f a = \prod a : Subtype p, f a$$$

Lean4

@[to_additive]
theorem prod_finset_coe (f : ι → M) (s : Finset ι) : (∏ i : (s : Set ι), f i) = ∏ i ∈ s, f i :=
  prod_coe_sort s f

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