mathlib documentation

data.list.sigma

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

List of keys from a list of key-value pairs

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

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

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

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

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

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

source
theorem list.not_eq_key {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a ∉ l.keys ↔ ∀ (s : sigma β), s ∈ l → a ≠ s.fst

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

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

source
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

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

source
@[simp]
theorem list.nodupkeys_cons {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :
(s :: l).nodupkeys ↔ s.fst ∉ l.keys ∧ l.nodupkeys

source
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) (a : s.fst = s'.fst) :
s = s'

source
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'

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

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

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

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

source
theorem list.nodupkeys_join {α : Type u} {β : α → Type v} {L : list (list (sigma β))} :
L.join.nodupkeys ↔ (∀ (l : list (sigma β)), l ∈ L → l.nodupkeys) ∧ list.pairwise list.disjoint (list.map list.keys L)

source
theorem list.nodup_enum_map_fst {α : Type u} (l : list α) :
(list.map prod.fst l.enum).nodup

source
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₁

source
def list.lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (a_1 : 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
source
@[simp]
theorem list.lookup_nil {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list.lookup a list.nil = none

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

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

source
theorem list.lookup_is_some {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
↥((list.lookup a l).is_some) ↔ a ∈ l.keys

source
theorem list.lookup_eq_none {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
list.lookup a l = none ↔ a ∉ l.keys

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

source
theorem list.mem_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : ⟨a, b⟩ ∈ l) :
b ∈ list.lookup a l

source
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

source
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

source
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₂

source
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₁

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

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

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

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

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

source
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

source
theorem list.head_lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
(list.lookup_all a l).head' = list.lookup a l

source
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

source
theorem list.lookup_all_sublist {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
list.map (sigma.mk a) (list.lookup_all a l) <+ l

source
theorem list.lookup_all_length_le_one {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
(list.lookup_all a l).length ≤ 1

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

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

source
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₂) :
list.lookup_all a l₁ = list.lookup_all a l₂

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

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

source
theorem list.kreplace_self {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : ⟨a, b⟩ ∈ l) :
list.kreplace a b l = l

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

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

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

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

Remove the first pair with the key a.

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

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

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

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

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

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

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

source
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₂

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

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

source
theorem list.kerase_kerase {α : 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)

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

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

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

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

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

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

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

source
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)

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

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

source
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

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

source
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₂

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

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

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

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

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

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

Equations
source
theorem list.erase_dupkeys_cons {α : Type u} {β : α → Type v} [decidable_eq α] {x : sigma β} (l : list (sigma β)) :
(x :: l).erase_dupkeys = list.kinsert x.fst x.snd l.erase_dupkeys

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

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

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

source
def list.kunion {α : Type u} {β : α → Type v} [decidable_eq α] (a a_1 : 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
source
@[simp]
theorem list.nil_kunion {α : Type u} {β : α → Type v} [decidable_eq α] {l : list (sigma β)} :
list.nil.kunion l = l

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

source
@[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₂)

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

source
@[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₂)

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

source
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

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

source
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₄

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

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

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

source
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₃)