English
Let ι be a finite type and t assign to each i a finite set, t(i). Then the product over the universal pi-tuple equals the product over the finite piFinset representation, with a natural encoding of arguments.
Русский
Пусть ι конечен, и для каждого i задан конечный набор t(i). Произведение по всем элементам унив-пи равно произведению по Finite-type piFinset с естественным отображением аргументов.
LaTeX
$$$\\prod x \\in \\mathrm{univ.pi}\\, t\\; f(x) = \\prod x \\in \\mathrm{Fintype.piFinset}\\, t\\; f\\big(\\lambda a, x(a)\\big).$$$
Lean4
/-- Taking a product over `univ.pi t` is the same as taking the product over `Fintype.piFinset t`.
`univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`, but differ
in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
`Fintype.piFinset t` is a `Finset (Π a, t a)`. -/
@[to_additive /-- Taking a sum over `univ.pi t` is the same as taking the sum over
`Fintype.piFinset t`. `univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`,
but differ in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
`Fintype.piFinset t` is a `Finset (Π a, t a)`. -/
]
theorem prod_univ_pi [DecidableEq ι] [Fintype ι] {κ : ι → Type*} (t : ∀ i, Finset (κ i))
(f : (∀ i ∈ (univ : Finset ι), κ i) → β) : ∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a _ ↦ x a := by
apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i) <;> simp
