Lists in product and sigma types #

This file proves basic properties of list.product and list.sigma, which are list constructions living in prod and sigma types respectively. Their definitions can be found in data.list.defs. Beware, this is not about list.prod, the multiplicative product.

product #

source

@[simp]

theorem list.nil_product {α : Type u_1} {β : Type u_2} (l : list β) :

list.nil.product l = list.nil

source

@[simp]

theorem list.product_cons {α : Type u_1} {β : Type u_2} (a : α) (l₁ : list α) (l₂ : list β) :

(a :: l₁).product l₂ = list.map (λ (b : β), (a, b)) l₂ ++ l₁.product l₂

source

@[simp]

theorem list.product_nil {α : Type u_1} {β : Type u_2} (l : list α) :

l.product list.nil = list.nil

source

@[simp]

theorem list.mem_product {α : Type u_1} {β : Type u_2} {l₁ : list α} {l₂ : list β} {a : α} {b : β} :

(a, b) ∈ l₁.product l₂ ↔ a ∈ l₁ ∧ b ∈ l₂

source

theorem list.length_product {α : Type u_1} {β : Type u_2} (l₁ : list α) (l₂ : list β) :

(l₁.product l₂).length = (l₁.length) * l₂.length

sigma #

source

@[simp]

theorem list.nil_sigma {α : Type u_1} {σ : α → Type u_3} (l : Π (a : α), list (σ a)) :

list.nil.sigma l = list.nil

source

@[simp]

theorem list.sigma_cons {α : Type u_1} {σ : α → Type u_3} (a : α) (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :

(a :: l₁).sigma l₂ = list.map (sigma.mk a) (l₂ a) ++ l₁.sigma l₂

source

@[simp]

theorem list.sigma_nil {α : Type u_1} {σ : α → Type u_3} (l : list α) :

l.sigma (λ (a : α), list.nil) = list.nil

source

@[simp]

theorem list.mem_sigma {α : Type u_1} {σ : α → Type u_3} {l₁ : list α} {l₂ : Π (a : α), list (σ a)} {a : α} {b : σ a} :

⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a

source

theorem list.length_sigma {α : Type u_1} {σ : α → Type u_3} (l₁ : list α) (l₂ : Π (a : α), list (σ a)) :

(l₁.sigma l₂).length = (list.map (λ (a : α), (l₂ a).length) l₁).sum