# Documentation

Mathlib.Data.Prod.TProd

# Finite products of types #

This file defines the product of types over a list. For l : List ι and α : ι → Type v 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 MeasureTheory.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.piEquivTProd below (or enhanced versions of it, like a MeasurableEquiv for product measures) to get the construction on ∀ i : ι, α i, at least when assuming [Fintype ι] [Encodable ι] (using Encodable.sortedUniv). Using local attribute [instance] Fintype.toEncodable we can get rid of the argument [Encodable ι].

## Main definitions #

• We have the equivalence TProd.piEquivTProd : (∀ i, α i) ≃ TProd α l if l contains every element of ι exactly once.
• The product of sets is Set.tprod : (∀ i, Set (α i)) → Set (TProd α l).
def List.TProd {ι : Type u} (α : ιType v) (l : List ι) :

The product of a family of types over a list.

Instances For
def List.TProd.mk {ι : Type u} {α : ιType v} (l : List ι) (_f : (i : ι) → α i) :

Turning a function f : ∀ i, α i into an element of the iterated product TProd α l.

Equations
Instances For
instance List.TProd.instInhabitedTProd {ι : Type u} {α : ιType v} {l : List ι} [(i : ι) → Inhabited (α i)] :
@[simp]
theorem List.TProd.fst_mk {ι : Type u} {α : ιType v} (i : ι) (l : List ι) (f : (i : ι) → α i) :
(List.TProd.mk (i :: l) f).fst = f i
@[simp]
theorem List.TProd.snd_mk {ι : Type u} {α : ιType v} (i : ι) (l : List ι) (f : (i : ι) → α i) :
(List.TProd.mk (i :: l) f).snd =
def List.TProd.elim {ι : Type u} {α : ιType v} [] {l : List ι} :
{i : ι} → i lα 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.

Equations
Instances For
@[simp]
theorem List.TProd.elim_self {ι : Type u} {α : ιType v} {i : ι} {l : List ι} [] (v : List.TProd α (i :: l)) :
List.TProd.elim v (_ : i i :: l) = v.fst
@[simp]
theorem List.TProd.elim_of_ne {ι : Type u} {α : ιType v} {i : ι} {j : ι} {l : List ι} [] (hj : j i :: l) (hji : j i) (v : List.TProd α (i :: l)) :
= List.TProd.elim v.snd (_ : j l)
@[simp]
theorem List.TProd.elim_of_mem {ι : Type u} {α : ιType v} {i : ι} {j : ι} {l : List ι} [] (hl : List.Nodup (i :: l)) (hj : j l) (v : List.TProd α (i :: l)) :
List.TProd.elim v (_ : j i :: l) = List.TProd.elim v.snd hj
theorem List.TProd.elim_mk {ι : Type u} {α : ιType v} [] (l : List ι) (f : (i : ι) → α i) {i : ι} (hi : i l) :
List.TProd.elim () hi = f i
theorem List.TProd.ext {ι : Type u} {α : ιType v} [] {l : List ι} :
∀ {v w : }, (∀ (i : ι) (hi : i l), = ) → v = w
def List.TProd.elim' {ι : Type u} {α : ιType v} {l : List ι} [] (h : ∀ (i : ι), i l) (v : ) (i : ι) :
α i

A version of TProd.elim when l contains all elements. In this case we get a function into Π i, α i.

Instances For
theorem List.TProd.mk_elim {ι : Type u} {α : ιType v} {l : List ι} [] (hnd : ) (h : ∀ (i : ι), i l) (v : ) :
= v
def List.TProd.piEquivTProd {ι : Type u} {α : ιType v} {l : List ι} [] (hnd : ) (h : ∀ (i : ι), i l) :
((i : ι) → α i)

Pi-types are equivalent to iterated products.

Instances For
def Set.tprod {ι : Type u} {α : ιType v} (l : List ι) (_t : (i : ι) → Set (α i)) :
Set ()

A product of sets in TProd α l.

Equations
Instances For
theorem Set.mk_preimage_tprod {ι : Type u} {α : ιType v} (l : List ι) (t : (i : ι) → Set (α i)) :
= Set.pi {i | i l} t
theorem Set.elim_preimage_pi {ι : Type u} {α : ιType v} [] {l : List ι} (hnd : ) (h : ∀ (i : ι), i l) (t : (i : ι) → Set (α i)) :
⁻¹' Set.pi Set.univ t =