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 (fun 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.

Main definitions #

@[reducible, inline]
abbrev List.TProd {ι : Type u} (α : ιType v) (l : List ι) :

The product of a family of types over a list.

Equations
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.instInhabited {ι : Type u} {α : ιType v} {l : List ι} [(i : ι) → Inhabited (α i)] :
      Equations
      @[simp]
      theorem List.TProd.fst_mk {ι : Type u} {α : ιType v} (i : ι) (l : List ι) (f : (i : ι) → α i) :
      (List.TProd.mk (i :: l) f).1 = f i
      @[simp]
      theorem List.TProd.snd_mk {ι : Type u} {α : ιType v} (i : ι) (l : List ι) (f : (i : ι) → α i) :
      def List.TProd.elim {ι : Type u} {α : ιType v} [DecidableEq ι] {l : List ι} :
      List.TProd α l{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
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem List.TProd.elim_self {ι : Type u} {α : ιType v} {i : ι} {l : List ι} [DecidableEq ι] (v : List.TProd α (i :: l)) :
        v.elim = v.1
        @[simp]
        theorem List.TProd.elim_of_ne {ι : Type u} {α : ιType v} {i : ι} {j : ι} {l : List ι} [DecidableEq ι] (hj : j i :: l) (hji : j i) (v : List.TProd α (i :: l)) :
        v.elim hj = List.TProd.elim v.2
        @[simp]
        theorem List.TProd.elim_of_mem {ι : Type u} {α : ιType v} {i : ι} {j : ι} {l : List ι} [DecidableEq ι] (hl : (i :: l).Nodup) (hj : j l) (v : List.TProd α (i :: l)) :
        v.elim = List.TProd.elim v.2 hj
        theorem List.TProd.elim_mk {ι : Type u} {α : ιType v} [DecidableEq ι] (l : List ι) (f : (i : ι) → α i) {i : ι} (hi : i l) :
        (List.TProd.mk l f).elim hi = f i
        theorem List.TProd.ext_iff {ι : Type u} {α : ιType v} [DecidableEq ι] {l : List ι} :
        ∀ {x : l.Nodup} {v w : List.TProd α l}, v = w ∀ (i : ι) (hi : i l), v.elim hi = w.elim hi
        theorem List.TProd.ext {ι : Type u} {α : ιType v} [DecidableEq ι] {l : List ι} :
        l.Nodup∀ {v w : List.TProd α l}, (∀ (i : ι) (hi : i l), v.elim hi = w.elim hi)v = w
        def List.TProd.elim' {ι : Type u} {α : ιType v} {l : List ι} [DecidableEq ι] (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
        Instances For
          theorem List.TProd.mk_elim {ι : Type u} {α : ιType v} {l : List ι} [DecidableEq ι] (hnd : l.Nodup) (h : ∀ (i : ι), i l) (v : List.TProd α l) :
          def List.TProd.piEquivTProd {ι : Type u} {α : ιType v} {l : List ι} [DecidableEq ι] (hnd : l.Nodup) (h : ∀ (i : ι), i l) :
          ((i : ι) → α i) List.TProd α l

          Pi-types are equivalent to iterated products.

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

            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)) :
              List.TProd.mk l ⁻¹' Set.tprod l t = {i : ι | i l}.pi t
              theorem Set.elim_preimage_pi {ι : Type u} {α : ιType v} [DecidableEq ι] {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