The cartesian product of lists

Main definitions

• List.pi: Cartesian product of lists indexed by a list.

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

• List.Pi.nil α a✝ a = nomatch a✝, a

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

• List.Pi.head f = f i ⋯

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

• List.Pi.tail f j hj = f j ⋯

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

• List.Pi.cons i l a f = Multiset.Pi.cons (↑l) i a f

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) : List.Pi.cons i l (List.Pi.head f) (List.Pi.tail f) = f

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 → α i → Prop} {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

• [].pi x = [List.Pi.nil α]
• (i :: l).pi x = (x i).bind fun (b : α i) => List.map (List.Pi.cons i l b) (l.pi x)

@[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