Documentation

Mathlib.Data.List.Pi

The cartesian product of lists #

Main definitions #

def List.Pi.nil {ι : Type u_1} (α : ιSort u_3) (i : ι) :
i []α i

Given α : ι → Sort*, Pi.nil α is the trivial dependent function out of the empty list.

Equations
    Instances For
      def List.Pi.head {ι : Type u_1} {α : ιSort u_2} {i : ι} {l : List ι} (f : (j : ι) → j i :: lα j) :
      α i

      Given f a function whose domain is i :: l, get its value at i.

      Equations
      Instances For
        def List.Pi.tail {ι : Type u_1} {α : ιSort u_2} {i : ι} {l : List ι} (f : (j : ι) → j i :: lα j) (j : ι) :
        j lα j

        Given f a function whose domain is i :: l, produce a function whose domain is restricted to l.

        Equations
        Instances For
          def List.Pi.cons {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} (i : ι) (l : List ι) (a : α i) (f : (j : ι) → j lα j) (j : ι) :
          j i :: lα j

          Given α : ι → Sort*, a list l and a term i, as well as a term a : α i and a function f such that f j : α j for all j in l, Pi.cons a f is a function g such that g k : α k for all k in i :: l.

          Equations
          Instances For
            theorem List.Pi.cons_def {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {i : ι} {l : List ι} (a : α i) (f : (j : ι) → j lα j) :
            List.Pi.cons i l a f = fun (j : ι) (hj : j i :: l) => if h : j = i then a else f j
            @[simp]
            theorem Multiset.Pi.cons_coe {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {i : ι} {l : List ι} (a : α i) (f : (j : ι) → j lα j) :
            Multiset.Pi.cons (↑l) i a f = List.Pi.cons i l a f
            @[simp]
            theorem List.Pi.cons_eta {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {i : ι} {l : List ι} (f : (j : ι) → j i :: lα j) :
            theorem List.Pi.cons_map {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {i : ι} {l : List ι} (a : α i) (f : (j : ι) → j lα j) {α' : ιSort u_3} (φ : j : ι⦄ → α jα' j) :
            (List.Pi.cons i l (φ a) fun (j : ι) (hj : j l) => φ (f j hj)) = fun (j : ι) (hj : j i :: l) => φ (List.Pi.cons i l a f j hj)
            theorem List.Pi.forall_rel_cons_ext {ι : Type u_1} [DecidableEq ι] {α : ιSort u_2} {i : ι} {l : List ι} {r : i : ι⦄ → α iα iProp} {a₁ : α i} {a₂ : α i} {f₁ : (j : ι) → j lα j} {f₂ : (j : ι) → j lα j} (ha : r a₁ a₂) (hf : ∀ (i : ι) (hi : i l), r (f₁ i hi) (f₂ i hi)) (j : ι) (hj : j i :: l) :
            r (List.Pi.cons i l a₁ f₁ j hj) (List.Pi.cons i l a₂ f₂ j hj)
            def List.pi {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} (l : List ι) :
            ((i : ι) → List (α i))List ((i : ι) → i lα i)

            pi xs f creates the list of functions g such that, for x ∈ xs, g x ∈ f x

            Equations
            Instances For
              @[simp]
              theorem List.pi_nil {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} (t : (i : ι) → List (α i)) :
              [].pi t = [List.Pi.nil α]
              @[simp]
              theorem List.pi_cons {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} (i : ι) (l : List ι) (t : (j : ι) → List (α j)) :
              (i :: l).pi t = (t i).bind fun (b : α i) => List.map (List.Pi.cons i l b) (l.pi t)
              theorem Multiset.pi_coe {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} (l : List ι) (fs : (i : ι) → List (α i)) :
              ((↑l).pi fun (x : ι) => (fs x)) = (l.pi fs)
              theorem List.mem_pi {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} {l : List ι} (fs : (i : ι) → List (α i)) (f : (i : ι) → i lα i) :
              f l.pi fs ∀ (i : ι) (hi : i l), f i hi fs i