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 β)} (h : 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} (l : 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 β)} (h : l.nodupkeys) :
list.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 β} (h : s l) (h' : s' l) :
s.fst = s'.fsts = s'

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

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

theorem list.nodupkeys_of_sublist {α : Type u} {β : α → Type v} {l₁ l₂ : list (sigma β)} (h : 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 β)} (h : l₁ ~ l₂) :

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 β)} (nd₀ : l₀.nodup) (nd₁ : l₁.nodup) (h : ∀ (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 β)} (nd : l.nodupkeys) (h : a, b⟩ 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 β)} (nd : 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 β)} (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) :
list.lookup a l₁ = list.lookup a l₂

theorem list.lookup_ext {α : Type u} {β : α → Type v} [decidable_eq α] {l₀ l₁ : list (sigma β)} (nd₀ : l₀.nodupkeys) (nd₁ : l₁.nodupkeys) (h : ∀ (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 β)} (h : l.nodupkeys) :

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

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

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

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

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

theorem list.kreplace_self {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : a, b⟩ 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 β)} (nd : l₁.nodupkeys) :
l₁ ~ l₂list.kreplace a b l₁ ~ list.kreplace a b l₂

def list.kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
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 β)} (h : a = s.fst) :
list.kerase a (s :: l) = l

@[simp]
theorem list.kerase_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} (h : a s.fst) :
list.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 β)} (h : a l.keys) :

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 β)} (h : 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 β)} (h : 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 β)} (nd : l₁.nodupkeys) :
l₁ ~ 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 β)} (nd : l.nodupkeys) :

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

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

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 : α) (b : β a) (l : list (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 β)} (nd : l.nodupkeys) :

theorem list.perm.kinsert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (p : l₁ ~ 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 β)} (h : a a') :

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 β)} (nd₁ : l₁.nodupkeys) (nd₂ : l₂.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 β)} (nd₃ : l₃.nodupkeys) (p₁₂ : l₁ ~ l₂) (p₃₄ : 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 β)} (h : a l₁.keys) :
list.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 β)} (h : a l₁.keys) :
list.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 β)} (h₁ : b list.lookup a (l₁.kunion l₃)) (h₂ : a l₂.keys) :
b list.lookup a ((l₁.kunion l₂).kunion l₃)