mathlib documentation

data.list.sigma

def list.keys {α : Type u} {β : α → Type v} :
list (sigma β)list α

List of keys from a list of key-value pairs

Equations
@[simp]
theorem list.keys_nil {α : Type u} {β : α → Type v} :

@[simp]
theorem list.keys_cons {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :
(s :: l).keys = s.fst :: l.keys

theorem list.mem_keys_of_mem {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :
s ls.fst l.keys

theorem list.exists_of_mem_keys {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a l.keys(∃ (b : β a), a, b⟩ l)

theorem list.mem_keys {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a l.keys ∃ (b : β a), a, b⟩ l

theorem list.not_mem_keys {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a l.keys ∀ (b : β a), a, b⟩ l

theorem list.not_eq_key {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a l.keys ∀ (s : sigma β), s la s.fst

def list.nodupkeys {α : Type u} {β : α → Type v} :
list (sigma β) → Prop

Equations
theorem list.nodupkeys_iff_pairwise {α : Type u} {β : α → Type v} {l : list (sigma β)} :
l.nodupkeys list.pairwise (λ (s s' : sigma β), s.fst s'.fst) l

theorem list.nodupkeys.pairwise_ne {α : Type u} {β : α → Type v} {l : list (sigma β)} :
l.nodupkeyslist.pairwise (λ (s s' : sigma β), s.fst s'.fst) l

@[simp]
theorem list.nodupkeys_nil {α : Type u} {β : α → Type v} :

@[simp]
theorem list.nodupkeys_cons {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :

theorem list.nodupkeys.eq_of_fst_eq {α : Type u} {β : α → Type v} {l : list (sigma β)} (nd : l.nodupkeys) {s s' : sigma β} :
s ls' ls.fst = s'.fsts = s'

theorem list.nodupkeys.eq_of_mk_mem {α : Type u} {β : α → Type v} {a : α} {b b' : β a} {l : list (sigma β)} :
l.nodupkeysa, b⟩ la, b'⟩ lb = b'

theorem list.nodupkeys_singleton {α : Type u} {β : α → Type v} (s : sigma β) :

theorem list.nodupkeys_of_sublist {α : Type u} {β : α → Type v} {l₁ l₂ : list (sigma β)} :
l₁ <+ l₂l₂.nodupkeys → l₁.nodupkeys

theorem list.nodup_of_nodupkeys {α : Type u} {β : α → Type v} {l : list (sigma β)} :

theorem list.perm_nodupkeys {α : Type u} {β : α → Type v} {l₁ l₂ : list (sigma β)} :
l₁ ~ l₂(l₁.nodupkeys l₂.nodupkeys)

theorem list.nodupkeys_join {α : Type u} {β : α → Type v} {L : list (list (sigma β))} :

theorem list.nodup_enum_map_fst {α : Type u} (l : list α) :

theorem list.mem_ext {α : Type u} {β : α → Type v} {l₀ l₁ : list (sigma β)} :
l₀.nodupl₁.nodup(∀ (x : sigma β), x l₀ x l₁)l₀ ~ l₁

def list.lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list (sigma β)option (β a)

lookup a l is the first value in l corresponding to the key a, or none if no such element exists.

Equations
@[simp]
theorem list.lookup_nil {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :

@[simp]
theorem list.lookup_cons_eq {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (Σ (a : α), β a)) (a : α) (b : β a) :
list.lookup a (a, b⟩ :: l) = some b

@[simp]
theorem list.lookup_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) {a : α} (s : sigma β) :
a s.fstlist.lookup a (s :: l) = list.lookup a l

theorem list.lookup_is_some {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :

theorem list.lookup_eq_none {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :

theorem list.of_mem_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b list.lookup a la, b⟩ l

theorem list.mem_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
l.nodupkeysa, b⟩ lb list.lookup a l

theorem list.map_lookup_eq_find {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
option.map (sigma.mk a) (list.lookup a l) = list.find (λ (s : sigma β), a = s.fst) l

theorem list.mem_lookup_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
l.nodupkeys(b list.lookup a l a, b⟩ l)

theorem list.perm_lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₂.nodupkeysl₁ ~ l₂list.lookup a l₁ = list.lookup a l₂

theorem list.lookup_ext {α : Type u} {β : α → Type v} [decidable_eq α] {l₀ l₁ : list (sigma β)} :
l₀.nodupkeysl₁.nodupkeys(∀ (x : α) (y : β x), y list.lookup x l₀ y list.lookup x l₁)l₀ ~ l₁

def list.lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list (sigma β)list (β a)

lookup_all a l is the list of all values in l corresponding to the key a.

Equations
@[simp]
theorem list.lookup_all_nil {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :

@[simp]
theorem list.lookup_all_cons_eq {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (Σ (a : α), β a)) (a : α) (b : β a) :

@[simp]
theorem list.lookup_all_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) {a : α} (s : sigma β) :

theorem list.lookup_all_eq_nil {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
list.lookup_all a l = list.nil ∀ (b : β a), a, b⟩ l

theorem list.head_lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :

theorem list.mem_lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b list.lookup_all a l a, b⟩ l

theorem list.lookup_all_sublist {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :

theorem list.lookup_all_length_le_one {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :

theorem list.lookup_all_eq_lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :

theorem list.lookup_all_nodup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :

theorem list.perm_lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₂.nodupkeysl₁ ~ l₂list.lookup_all a l₁ = list.lookup_all a l₂

def list.kreplace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
β alist (sigma β)list (sigma β)

Equations
theorem list.kreplace_of_forall_not {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} :
(∀ (b : β a), a, b⟩ l)list.kreplace a b l = l

theorem list.kreplace_self {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
l.nodupkeysa, b⟩ llist.kreplace a b l = l

theorem list.keys_kreplace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (l : list (sigma β)) :

theorem list.kreplace_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} :

theorem list.perm.kreplace {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₁ ~ l₂list.kreplace a b l₁ ~ list.kreplace a b l₂

def list.kerase {α : Type u} {β : α → Type v} [decidable_eq α] :
α → list (sigma β)list (sigma β)

Remove the first pair with the key a.

Equations
@[simp]
theorem list.kerase_nil {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} :

@[simp]
theorem list.kerase_cons_eq {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} :
a = s.fstlist.kerase a (s :: l) = l

@[simp]
theorem list.kerase_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} :
a s.fstlist.kerase a (s :: l) = s :: list.kerase a l

@[simp]
theorem list.kerase_of_not_mem_keys {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
a l.keyslist.kerase a l = l

theorem list.kerase_sublist {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :

theorem list.kerase_keys_subset {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :

theorem list.mem_keys_of_mem_keys_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a₁ a₂ : α} {l : list (sigma β)} :
a₁ (list.kerase a₂ l).keysa₁ l.keys

theorem list.exists_of_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
a l.keys(∃ (b : β a) (l₁ l₂ : list (sigma β)), a l₁.keys l = l₁ ++ a, b⟩ :: l₂ list.kerase a l = l₁ ++ l₂)

@[simp]
theorem list.mem_keys_kerase_of_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a₁ a₂ : α} {l : list (sigma β)} :
a₁ a₂(a₁ (list.kerase a₂ l).keys a₁ l.keys)

theorem list.keys_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :

theorem list.kerase_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {l : list (sigma β)} :

theorem list.kerase_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :

theorem list.perm.kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₁ ~ l₂list.kerase a l₁ ~ list.kerase a l₂

@[simp]
theorem list.not_mem_keys_kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :

@[simp]
theorem list.lookup_kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :

@[simp]
theorem list.lookup_kerase_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {l : list (sigma β)} :
a a'list.lookup a (list.kerase a' l) = list.lookup a l

theorem list.kerase_append_left {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a l₁.keyslist.kerase a (l₁ ++ l₂) = list.kerase a l₁ ++ l₂

theorem list.kerase_append_right {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a l₁.keyslist.kerase a (l₁ ++ l₂) = l₁ ++ list.kerase a l₂

theorem list.kerase_comm {α : Type u} {β : α → Type v} [decidable_eq α] (a₁ a₂ : α) (l : list (sigma β)) :
list.kerase a₂ (list.kerase a₁ l) = list.kerase a₁ (list.kerase a₂ l)

theorem list.sizeof_kerase {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [has_sizeof (sigma β)] (x : α) (xs : list (sigma β)) :

def list.kinsert {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
β alist (sigma β)list (sigma β)

Insert the pair ⟨a, b⟩ and erase the first pair with the key a.

Equations
@[simp]
theorem list.kinsert_def {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
list.kinsert a b l = a, b⟩ :: list.kerase a l

theorem list.mem_keys_kinsert {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b' : β a'} {l : list (sigma β)} :
a (list.kinsert a' b' l).keys a = a' a l.keys

theorem list.kinsert_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} :

theorem list.perm.kinsert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₁ ~ l₂list.kinsert a b l₁ ~ list.kinsert a b l₂

theorem list.lookup_kinsert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} (l : list (sigma β)) :

theorem list.lookup_kinsert_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b' : β a'} {l : list (sigma β)} :
a a'list.lookup a (list.kinsert a' b' l) = list.lookup a l

def list.kextract {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list (sigma β)option (β a) × list (sigma β)

Equations
@[simp]
theorem list.kextract_eq_lookup_kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :

def list.erase_dupkeys {α : Type u} {β : α → Type v} [decidable_eq α] :
list (sigma β)list (sigma β)

Remove entries with duplicate keys from l : list (sigma β).

Equations
theorem list.erase_dupkeys_cons {α : Type u} {β : α → Type v} [decidable_eq α] {x : sigma β} (l : list (sigma β)) :

theorem list.nodupkeys_erase_dupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) :

theorem list.lookup_erase_dupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :

theorem list.sizeof_erase_dupkeys {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [has_sizeof (sigma β)] (xs : list (sigma β)) :

def list.kunion {α : Type u} {β : α → Type v} [decidable_eq α] :
list (sigma β)list (sigma β)list (sigma β)

kunion l₁ l₂ is the append to l₁ of l₂ after, for each key in l₁, the first matching pair in l₂ is erased.

Equations
@[simp]
theorem list.nil_kunion {α : Type u} {β : α → Type v} [decidable_eq α] {l : list (sigma β)} :

@[simp]
theorem list.kunion_nil {α : Type u} {β : α → Type v} [decidable_eq α] {l : list (sigma β)} :

@[simp]
theorem list.kunion_cons {α : Type u} {β : α → Type v} [decidable_eq α] {s : sigma β} {l₁ l₂ : list (sigma β)} :
(s :: l₁).kunion l₂ = s :: l₁.kunion (list.kerase s.fst l₂)

@[simp]
theorem list.mem_keys_kunion {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a (l₁.kunion l₂).keys a l₁.keys a l₂.keys

@[simp]
theorem list.kunion_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
(list.kerase a l₁).kunion (list.kerase a l₂) = list.kerase a (l₁.kunion l₂)

theorem list.kunion_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₂.nodupkeys(l₁.kunion l₂).nodupkeys

theorem list.perm.kunion_right {α : Type u} {β : α → Type v} [decidable_eq α] {l₁ l₂ : list (sigma β)} (p : l₁ ~ l₂) (l : list (sigma β)) :
l₁.kunion l ~ l₂.kunion l

theorem list.perm.kunion_left {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) {l₁ l₂ : list (sigma β)} :
l₁.nodupkeysl₁ ~ l₂l.kunion l₁ ~ l.kunion l₂

theorem list.perm.kunion {α : Type u} {β : α → Type v} [decidable_eq α] {l₁ l₂ l₃ l₄ : list (sigma β)} :
l₃.nodupkeysl₁ ~ l₂l₃ ~ l₄l₁.kunion l₃ ~ l₂.kunion l₄

@[simp]
theorem list.lookup_kunion_left {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a l₁.keyslist.lookup a (l₁.kunion l₂) = list.lookup a l₁

@[simp]
theorem list.lookup_kunion_right {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a l₁.keyslist.lookup a (l₁.kunion l₂) = list.lookup a l₂

@[simp]
theorem list.mem_lookup_kunion {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} :
b list.lookup a (l₁.kunion l₂) b list.lookup a l₁ a l₁.keys b list.lookup a l₂

theorem list.mem_lookup_kunion_middle {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ l₃ : list (sigma β)} :
b list.lookup a (l₁.kunion l₃)a l₂.keysb list.lookup a ((l₁.kunion l₂).kunion l₃)