prod_eq_prod_extend — Mathlib

English

Let f : s → M be a function on a finite set s (as a subset), and extend it to a function on the ambient type by defining extend f 1 x = f x if x ∈ s and 1 otherwise. Then the total product over the ambient finite set equals the product over s of f.

Русский

Пусть f : s → M; расширение функции to всю оболочку задаёт extend f 1 x, который равен f x при x ∈ s и 1 иначе; тогда общее произведение совпадает с произведением по s.

LaTeX

$$$\displaystyle \prod x, f x = \prod x \in s, extend f 1 x$$$

Lean4

@[to_additive]
theorem prod_eq_prod_extend (f : s → M) : ∏ x, f x = ∏ x ∈ s, Subtype.val.extend f 1 x :=
  by
  rw [univ_eq_attach, ← Finset.prod_attach s]
  congr with ⟨x, hx⟩
  rw [Subtype.val_injective.extend_apply]

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