mathlib3 documentation

data.prod.tprod

Finite products of types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_tprod below (or enhanced versions of it, like a measurable_equiv for product measures) to get the construction on Π i : ι, α i, at least when assuming [fintype ι] [encodable ι] (using encodable.sorted_univ). Using local attribute [instance] fintype.to_encodable we can get rid of the argument [encodable ι].

Main definitions #

We have the equivalence tprod.pi_equiv_tprod : (Π 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_1} (α : ι → Type u_2) (l : list ι) :

Type (max u_2 u_3)

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

Instances for list.tprod

@[protected]

def list.tprod.mk {ι : Type u_1} {α : ι → Type u_2} (l : list ι) (f : Π (i : ι), α i) :

list.tprod α 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

@[protected, instance]

def list.tprod.inhabited {ι : Type u_1} {α : ι → Type u_2} {l : list ι} [Π (i : ι), inhabited (α i)] :

inhabited (list.tprod α l)

Equations

list.tprod.inhabited = {default := list.tprod.mk l inhabited.default}

@[simp]

theorem list.tprod.fst_mk {ι : Type u_1} {α : ι → Type u_2} (i : ι) (l : list ι) (f : Π (i : ι), α i) :

(list.tprod.mk (i :: l) f).fst = f i

@[simp]

theorem list.tprod.snd_mk {ι : Type u_1} {α : ι → Type u_2} (i : ι) (l : list ι) (f : Π (i : ι), α i) :

(list.tprod.mk (i :: l) f).snd = list.tprod.mk l f

@[protected]

def list.tprod.elim {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] {l : list ι} (v : list.tprod α l) {i : ι} (hi : 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

v.elim hj = dite (j = i) (λ (hji : j = i), eq.rec (λ (v : list.tprod α (j :: is)) (hj : j ∈ j :: is), v.fst) hji v hj) (λ (hji : ¬j = i), list.tprod.elim v.snd _)

@[simp]

theorem list.tprod.elim_self {ι : Type u_1} {α : ι → Type u_2} {i : ι} {l : list ι} [decidable_eq ι] (v : list.tprod α (i :: l)) :

v.elim _ = v.fst

@[simp]

theorem list.tprod.elim_of_ne {ι : Type u_1} {α : ι → Type u_2} {i j : ι} {l : list ι} [decidable_eq ι] (hj : j ∈ i :: l) (hji : j ≠ i) (v : list.tprod α (i :: l)) :

v.elim hj = list.tprod.elim v.snd _

@[simp]

theorem list.tprod.elim_of_mem {ι : Type u_1} {α : ι → Type u_2} {i j : ι} {l : list ι} [decidable_eq ι] (hl : (i :: l).nodup) (hj : j ∈ l) (v : list.tprod α (i :: l)) :

v.elim _ = list.tprod.elim v.snd hj

theorem list.tprod.elim_mk {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] (l : list ι) (f : Π (i : ι), α i) {i : ι} (hi : i ∈ l) :

(list.tprod.mk l f).elim hi = f i

@[ext]

theorem list.tprod.ext {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] {l : list ι} (hl : l.nodup) {v w : list.tprod α l} (hvw : ∀ (i : ι) (hi : i ∈ l), v.elim hi = w.elim hi) :

v = w

@[protected, simp]

def list.tprod.elim' {ι : Type u_1} {α : ι → Type u_2} {l : list ι} [decidable_eq ι] (h : ∀ (i : ι), i ∈ l) (v : list.tprod α l) (i : ι) :

α 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 _

theorem list.tprod.mk_elim {ι : Type u_1} {α : ι → Type u_2} {l : list ι} [decidable_eq ι] (hnd : l.nodup) (h : ∀ (i : ι), i ∈ l) (v : list.tprod α l) :

list.tprod.mk l (list.tprod.elim' h v) = v

def list.tprod.pi_equiv_tprod {ι : Type u_1} {α : ι → Type u_2} {l : list ι} [decidable_eq ι] (hnd : l.nodup) (h : ∀ (i : ι), i ∈ l) :

(Π (i : ι), α i) ≃ list.tprod α l

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 := _}

@[protected, simp]

def set.tprod {ι : Type u_1} {α : ι → Type u_2} (l : list ι) (t : Π (i : ι), set (α i)) :

set (list.tprod α l)

A product of sets in tprod α l.

Equations

set.tprod (i :: is) t = t i ×ˢ set.tprod is t
set.tprod list.nil t = set.univ

theorem set.mk_preimage_tprod {ι : Type u_1} {α : ι → Type u_2} (l : list ι) (t : Π (i : ι), set (α i)) :

list.tprod.mk l ⁻¹' set.tprod l t = {i : ι | i ∈ l}.pi t

theorem set.elim_preimage_pi {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] {l : list ι} (hnd : l.nodup) (h : ∀ (i : ι), i ∈ l) (t : Π (i : ι), set (α i)) :

list.tprod.elim' h ⁻¹' set.univ.pi t = set.tprod l t