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 typetprod 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_tprod
below (or enhanced versions of it, like ameasurable_equiv
for product measures) to get the construction onΠ i : ι, α i
, at least when assuming[fintype ι] [encodable ι]
(usingencodable.sorted_univ
). Usinglocal attribute [instance] fintype.encodable
we can get rid of the argument[encodable ι]
.
Main definitions #
The product of a family of types over a list.
Equations
- list.tprod α l = list.foldr (λ (i : ι) (β : Type (max u_2 u_3)), α i × β) punit l
Turning a function f : Π i, α i
into an element of the iterated product tprod α l
.
Equations
- list.tprod.mk (i :: is) = λ (f : Π (i : ι), α i), (f i, list.tprod.mk is f)
- list.tprod.mk list.nil = λ (f : Π (i : ι), α i), punit.star
Equations
- list.tprod.inhabited = {default := list.tprod.mk l (λ (i : ι), default (α i))}
Given an element of the iterated product l.prod α
, take a projection into direction i
.
If i
appears multiple times in l
, this chooses the first component in direction i
.
A version of tprod.elim
when l
contains all elements. In this case we get a function into
Π i, α i
.
Equations
- list.tprod.elim' h v i = v.elim _
Pi-types are equivalent to iterated products.
Equations
- list.tprod.pi_equiv_tprod hnd h = {to_fun := list.tprod.mk l, inv_fun := list.tprod.elim' h, left_inv := _, right_inv := _}