Documentation

Mathlib.Data.List.ProdSigma

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 #

@[simp]
theorem List.nil_product {α : Type u_1} {β : Type u_2} (l : List β) :
[] ×ˢ l = []
@[simp]
theorem List.product_cons {α : Type u_1} {β : Type u_2} (a : α) (l₁ : List α) (l₂ : List β) :
(a :: l₁) ×ˢ l₂ = List.map (fun (b : β) => (a, b)) l₂ ++ l₁ ×ˢ l₂
@[simp]
theorem List.product_nil {α : Type u_1} {β : Type u_2} (l : List α) :
l ×ˢ [] = []
@[simp]
theorem List.mem_product {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {a : α} {b : β} :
(a, b) l₁ ×ˢ l₂ a l₁ b l₂
theorem List.length_product {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
List.length (l₁ ×ˢ l₂) = List.length l₁ * List.length l₂

sigma #

@[simp]
theorem List.nil_sigma {α : Type u_1} {σ : αType u_3} (l : (a : α) → List (σ a)) :
List.sigma [] l = []
@[simp]
theorem List.sigma_cons {α : Type u_1} {σ : αType u_3} (a : α) (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
List.sigma (a :: l₁) l₂ = List.map (Sigma.mk a) (l₂ a) ++ List.sigma l₁ l₂
@[simp]
theorem List.sigma_nil {α : Type u_1} {σ : αType u_3} (l : List α) :
(List.sigma l fun (a : α) => []) = []
@[simp]
theorem List.mem_sigma {α : Type u_1} {σ : αType u_3} {l₁ : List α} {l₂ : (a : α) → List (σ a)} {a : α} {b : σ a} :
{ fst := a, snd := b } List.sigma l₁ l₂ a l₁ b l₂ a
theorem List.length_sigma {α : Type u_1} {σ : αType u_3} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
List.length (List.sigma l₁ l₂) = List.sum (List.map (fun (a : α) => List.length (l₂ a)) l₁)