Finite products of types #
This file defines the product of types over a list. For
l : list ι and
α : ι → Type* we define
list.tprod α l = l.foldr (λ i β, α i × β) punit.
This type should not be used if
Π i, α i or
Π i ∈ l, α i can be used instead
(in the last expression, we could also replace the list
l by a set or a finset).
This type is used as an intermediary between binary products and finitary products.
The application of this type is finitary product measures, but it could be used in any
construction/theorem that is easier to define/prove on binary products than on finitary products.
- Once we have the construction on binary products (like binary product measures in
measure_theory.prod), we can easily define a finitary version on the type
tprod l αby iterating. Properties can also be easily extended from the binary case to the finitary case by iterating.
- Then we can use the equivalence
list.tprod.pi_equiv_tprodbelow (or enhanced versions of it, like a
measurable_equivfor product measures) to get the construction on
Π i : ι, α i, at least when assuming
[fintype ι] [encodable ι](using
local attribute [instance] fintype.encodablewe can get rid of the argument
Main definitions #
Turning a function
f : Π i, α i into an element of the iterated product
tprod α l.
Given an element of the iterated product
l.prod α, take a projection into direction
i appears multiple times in
l, this chooses the first component in direction
A version of
l contains all elements. In this case we get a function into
Π i, α i.
Pi-types are equivalent to iterated products.