Module docstring
{"# Products over univ.pi
"}
Finset.prod_univ_pi
theorem
[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
Full source
/-- 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)`."]
lemma 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) <;> simpInformal description
Let $\iota$ be a finite type with decidable equality, and for each $i \in \iota$, let $\kappa(i)$ be a type with a finite subset $t(i) \subseteq \kappa(i)$. Given a function $f \colon \left(\prod_{i \in \iota} \kappa(i)\right) \to \beta$ where $\beta$ is a commutative monoid, the product of $f$ over the finite set $\text{univ.pi}\, t$ is equal to the product of $f$ over the finite set $\text{Fintype.piFinset}\, t$. Here, $\text{univ.pi}\, t$ is the set of dependent functions $x$ such that $x(i) \in t(i)$ for all $i \in \iota$, and $\text{Fintype.piFinset}\, t$ is the set of functions $x \colon \iota \to \bigcup_{i \in \iota} \kappa(i)$ such that $x(i) \in t(i)$ for all $i \in \iota$.