prod_attach_index — Mathlib

English

For any finite set s and function f : α → M, we have ∏ x ∈ s.attach, h x (f x) = ∏ x ∈ s, h x (f x).

Русский

Для любого конечного множества s и функции f : α → M выполняется равенство произведений по x ∈ s.attach и по x ∈ s.

LaTeX

$$$\prod_{x \in s.attach} h\ x\ (f x) = \prod_{x \in s} h\ x\ (f x).$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_attach_index [CommMonoid N] {s : Finset α} (f : α → M) {h : α → M → N} :
    ∏ x ∈ s.attach, h x (f x) = ∏ x ∈ s, h x (f x) :=
  prod_attach _ fun x ↦ h x (f x)

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