structure Map (α : Type u) (β : Type v) [hh₁ : DecidableEq α] [hh₂ : Hashable α] : Type (max u v)

• inner : Std.ExtDHashMap α fun (x : α) => β

@[instance_reducible]

instance instInhabitedMap {a✝ : Type u_1} {a✝¹ : Type u_2} {a✝² : DecidableEq a✝} {a✝³ : Hashable a✝} : Inhabited (Map a✝ a✝¹)

Equations

• instInhabitedMap = { default := instInhabitedMap.default }

def Map.empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : Map α β

Equations

• Map.empty = { inner := ∅ }

@[instance_reducible]

instance Map.instEmptyCollection {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : EmptyCollection (Map α β)

Equations

• Map.instEmptyCollection = { emptyCollection := Map.empty }

theorem Map.empty_def {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : ∅ = { inner := ∅ }

def Map.insertP {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (x : α × β) (mp : Map α β) : Map α β

Equations

• Map.insertP x mp = { inner := insert x.toSigma mp.inner }

@[instance_reducible]

instance Map.instInsertProd {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : Insert (α × β) (Map α β)

Equations

• Map.instInsertProd = { insert := Map.insertP }

theorem Map.insert_def {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {x : α × β} {mp : Map α β} : insert x mp = { inner := insert x.toSigma mp.inner }

def Map.insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (i : α) (x : β) : Map α β

Equations

• mp.insert i x = { inner := mp.inner.insert i x }

def Map.ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (xs : List (α × β)) : Map α β

Equations

• Map.ofList xs = { inner := Std.ExtDHashMap.ofList (List.map Prod.toSigma xs) }

def Map.get? {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (i : α) (mp : Map α β) : Option β

Equations

• Map.get? i mp = mp.inner.get? i

def Map.get! {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (i : α) [h : Inhabited β] (mp : Map α β) : β

Equations

• Map.get! i mp = mp.inner.get! i

def Map.map {α : Type u} {β : Type v} {γ : Type w} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (f : α → β → γ) : Map α γ

Equations

• mp.map f = { inner := Std.ExtDHashMap.map f mp.inner }

def Map.mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (i : α) : Prop

Equations

• mp.mem i = (i ∈ mp.inner)

@[instance_reducible]

instance Map.instMembership {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : Membership α (Map α β)

Equations

• Map.instMembership = { mem := Map.mem }

theorem Map.mem_def {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} : i ∈ mp ↔ i ∈ mp.inner

@[instance_reducible]

instance Map.instDecidableMem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} : Decidable (mp.mem i)

Equations

• Map.instDecidableMem = id inferInstance

@[instance_reducible]

instance Map.instDecidableMem_1 {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} : Decidable (i ∈ mp)

Equations

• Map.instDecidableMem_1 = id inferInstance

theorem Map.mem_iff_get?_eq_some {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} : i ∈ mp ↔ ∃ (x : β), get? i mp = some x

theorem Map.get?_eq_some_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} (h : i ∈ mp) : ∃ (x : β), get? i mp = some x

theorem Map.get?_eq_none_of_not_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} (h : i ∉ mp) : get? i mp = none

@[simp]

theorem Map.get?_eq_none_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} : get? i mp = none ↔ i ∉ mp

theorem Map.get?_map {α : Type u} {β : Type v} {γ : Type w} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {f : α → β → γ} {i : α} : get? i (mp.map f) = Option.map (f i) (get? i mp)

theorem Map.get!_map_eq_of_pos {α : Type u} {β : Type v} {γ : Type w} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {f : α → β → γ} {i : α} [ha : Inhabited β] [hb : Inhabited γ] (h : i ∈ mp) : get! i (mp.map f) = f i (get! i mp)

def Map.toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : Map α β) : List (α × β)

Equations

• mp.toList = Std.ExtDHashMap.lift (fun (m : Std.DHashMap α fun (i : α) => β) => List.map Sigma.toProd m.toSortedList) ⋯ mp.inner

@[simp]

theorem Map.ofList_nil {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : ofList [] = ∅

@[simp]

theorem Map.ofList_snoc {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} {x : α × β} : ofList (xs ++ [x]) = insertP x (ofList xs)

@[simp]

theorem Map.toList_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] : ∅.toList = []

@[simp]

theorem Map.mem_insertP {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {x : α × β} {i : α} : i ∈ insertP x mp ↔ i = x.1 ∨ i ∈ mp

@[simp]

theorem Map.mem_insert' {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} {j : α} : j ∈ mp.insert i x ↔ j = i ∨ j ∈ mp

@[simp]

theorem Map.mem_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {x : α × β} {i : α} : i ∈ insert x mp ↔ i = x.1 ∨ i ∈ mp

@[simp]

theorem Map.mem_ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} {i : α} : i ∈ ofList xs ↔ ∃ (x : β), (i, x) ∈ xs

@[simp]

theorem Map.mem_map {α : Type u} {β : Type v} {γ : Type w} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {f : α → β → γ} {i : α} : i ∈ mp.map f ↔ i ∈ mp

theorem Map.eq_empty_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} : mp = ∅ ↔ ∀ (i : α), i ∉ mp

@[simp]

theorem Map.not_mem_empty' {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i : α} : ¬∅.mem i

@[simp]

theorem Map.not_mem_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i : α} : i ∉ ∅

theorem Map.ext_iff' {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ = m₂ ↔ m₁.inner.inner.out.Equiv m₂.inner.inner.out

theorem Map.ext' {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} (h : m₁.inner.inner.out.Equiv m₂.inner.inner.out) : m₁ = m₂

theorem Map.ext_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ = m₂ ↔ ∀ (i : α), get? i m₁ = get? i m₂

theorem Map.ext {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} (h : ∀ (i : α), get? i m₁ = get? i m₂) : m₁ = m₂

theorem Map.get?_eq_ite_of_unit {α : Type u} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Map α Unit} {i : α} : get? i m = if i ∈ m then some () else none

@[simp]

theorem Map.get?_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i : α} : get? i ∅ = none

theorem Map.ofList_eq_ofList_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs ys : List (α × β)} (hx : (List.map (fun (x : α × β) => x.1) xs).Nodup) (hy : (List.map (fun (x : α × β) => x.1) ys).Nodup) : ofList xs = ofList ys ↔ xs.Perm ys

def Map.range {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] (f : α → β) : Map α β

Equations

• Map.range f = { inner := Std.ExtDHashMap.range f }

@[simp]

theorem Map.mem_range {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f : α → β} {i : α} : i ∈ range f

@[simp]

theorem Map.nonempty_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {x : α × β} : insert x mp ≠ ∅

@[simp]

theorem Map.nodup_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [LinearOrder α] : mp.toList.Nodup

@[simp]

theorem Map.pairwise_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [LinearOrder α] : List.Pairwise (fun (x1 x2 : α × β) => x1.1 ≤ x2.1) mp.toList

@[simp]

theorem Map.mem_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [LinearOrder α] {x : α × β} : x ∈ mp.toList ↔ get? x.1 mp = some x.2

@[simp]

theorem Map.toList_eq_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : Map α β} : m₁.toList = m₂.toList ↔ m₁ = m₂

@[simp]

theorem Map.toList_eq_nil_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [LinearOrder α] : mp.toList = [] ↔ mp = ∅

def Map.toDMap {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) : DMap α fun (x : α) => β

Equations

• mp.toDMap = { inner := mp.inner }

def DMap.toMap {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : DMap α fun (x : α) => β) : Map α β

Equations

• mp.toMap = { inner := mp.inner }

@[instance_reducible]

instance Map.instDecidableEq {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : DecidableEq β] : DecidableEq (Map α β)

Equations

• m₁.instDecidableEq m₂ = match h : decide (m₁.inner = m₂.inner) with | true => isTrue ⋯ | false => isFalse ⋯

def Map.values {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : Map α β) : List β

Equations

• mp.values = List.map (fun (x : α × β) => x.2) mp.toList

def Map.all {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (p : α → β → Bool) : Bool

Equations

• mp.all p = mp.inner.all p

@[simp]

theorem Map.all_def {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [LinearOrder α] {p : α → β → Bool} : mp.all p = decide (∀ x ∈ mp.toList, p x.1 x.2 = true)

def Map.modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (i : α) (f : β → β) : Map α β

Equations

• mp.modify i f = { inner := mp.inner.modify i f }

def Map.modifyMany {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (xs : List (α × (β → β))) : Map α β

Equations

• mp.modifyMany xs = { inner := mp.inner.modifyMany (List.map (fun (x : α × (β → β)) => x.toSigma) xs) }

@[simp]

theorem Map.modifyMany_nil {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} : mp.modifyMany [] = mp

@[simp]

theorem Map.modifyMany_cons {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β → β} {xs : List (α × (β → β))} : mp.modifyMany ((i, x) :: xs) = (mp.modify i x).modifyMany xs

def Map.insertMany {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (xs : List (α × β)) : Map α β

Equations

• mp.insertMany xs = { inner := mp.inner.insertMany (List.map (fun (x : α × β) => x.toSigma) xs) }

@[simp]

theorem Map.insertMany_nil {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} : mp.insertMany [] = mp

@[simp]

theorem Map.insertMany_cons {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} {xs : List (α × β)} : mp.insertMany ((i, x) :: xs) = (mp.insert i x).insertMany xs

theorem Map.get?_eq_ite {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [hb : Inhabited β] {i : α} : get? i mp = if i ∈ mp then some (get! i mp) else none

@[simp]

theorem Map.mem_modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i j : α} {x : β → β} : i ∈ mp.modify j x ↔ i ∈ mp

theorem Map.get!_eq_get?_get! {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [Inhabited β] {i : α} : get! i mp = (get? i mp).get!

@[simp]

theorem Map.get?_modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {f : β → β} {j : α} : get? j (mp.modify i f) = if j = i then Option.map f (get? j mp) else get? j mp

@[simp]

theorem Map.mem_values {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [LinearOrder α] {x : β} : x ∈ mp.values ↔ ∃ (i : α), get? i mp = some x

@[instance_reducible]

instance Map.instFintype {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] [hb : Fintype β] : Fintype (Map α β)

Equations

• Map.instFintype = { elems := Finset.map { toFun := Map.mk, inj' := ⋯ } Fintype.elems, complete := ⋯ }

instance Map.instFinite {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Finite α] [hb : Finite β] : Finite (Map α β)

@[simp]

theorem Map.range_eq_range_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f g : α → β} : range f = range g ↔ ∀ (x : α), f x = g x

theorem Map.mem_of_get?_eq_some {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} (h : get? i mp = some x) : i ∈ mp

theorem Map.get!_eq_get!_get? {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} [hb : Inhabited β] : get! i mp = (get? i mp).get!

@[simp]

theorem Map.get?_eq_some_get!_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} [hb : Inhabited β] : get? i mp = some (get! i mp) ↔ i ∈ mp

@[simp]

theorem Map.get?_eq_some_get?_get! {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} [hb : Inhabited β] : get? i mp = some (get? i mp).get! ↔ i ∈ mp

def Map.fold {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_1} (mp : Map α β) (f : γ → α → β → γ) (z : γ) (h_assoc : ∀ {acc : γ} {i : α} {x : β} {j : α} {y : β}, i ≠ j → f (f acc i x) j y = f (f acc j y) i x) : γ

Equations

• mp.fold f z h_assoc = mp.inner.fold f z ⋯

theorem Map.fold_eq_foldl_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {γ : Type u_1} {z : γ} {f : γ → α → β → γ} {h_assoc : ∀ {acc : γ} {i : α} {x : β} {j : α} {y : β}, i ≠ j → f (f acc i x) j y = f (f acc j y) i x} : mp.fold f z h_assoc = List.foldl (fun (acc : γ) (x : α × β) => f acc x.1 x.2) z mp.toList

theorem Map.eq_iff_inner_eq {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ = m₂ ↔ m₁.inner = m₂.inner

theorem Map.eq_iff_toList_eq {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {m₁ m₂ : Map α β} : m₁ = m₂ ↔ m₁.toList = m₂.toList

@[simp]

theorem Map.ofList_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : ofList mp.toList = mp

theorem Map.toList_ofList_perm {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List (α × β)} (h : (List.map (fun (x : α × β) => x.1) xs).Nodup) : (ofList xs).toList.Perm xs

def Map.keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : Map α β) : List α

Equations

• mp.keys = mp.inner.keys

@[simp]

theorem Map.sortedLE_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.keys.SortedLE

@[simp]

theorem Map.sortedLT_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.keys.SortedLT

theorem Map.keys_eq_map_fst_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.keys = List.map (fun (x : α × β) => x.1) mp.toList

def Map.minKey? {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : Map α β) : Option α

Equations

• mp.minKey? = mp.inner.minKey?

def Map.maxKey? {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : Map α β) : Option α

Equations

• mp.maxKey? = mp.inner.maxKey?

def Map.minKey! {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (mp : Map α β) : α

Equations

• mp.minKey! = mp.minKey?.get!

def Map.maxKey! {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (mp : Map α β) : α

Equations

• mp.maxKey! = mp.maxKey?.get!

theorem Map.minKey?_eq_head?_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.minKey? = mp.keys.head?

theorem Map.maxKey?_eq_getLast?_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.maxKey? = mp.keys.getLast?

@[simp]

theorem Map.minKey?_eq_none_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.minKey? = none ↔ mp = ∅

@[simp]

theorem Map.maxKey?_eq_none_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.maxKey? = none ↔ mp = ∅

theorem Map.not_mem_of_lt_minKey? {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.minKey? = some m) (h₂ : x < m) : x ∉ mp

theorem Map.not_mem_of_maxKey?_lt {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.maxKey? = some m) (h₂ : m < x) : x ∉ mp

theorem Map.not_mem_of_lt_minKey! {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : x < mp.minKey!) : x ∉ mp

theorem Map.not_mem_of_maxKey!_lt {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : mp.maxKey! < x) : x ∉ mp

theorem Map.minKey?_le_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.minKey? = some m) (h₂ : x ∈ mp) : m ≤ x

theorem Map.le_maxKey?_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.maxKey? = some m) (h₂ : x ∈ mp) : x ≤ m

theorem Map.minKey!_le_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : x ∈ mp) : mp.minKey! ≤ x

theorem Map.le_maxKey!_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : x ∈ mp) : x ≤ mp.maxKey!

theorem Map.ind {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : Map α β → Prop} (h₁ : p ∅) (h₂ : ∀ (m : Map α β) (i : α) (x : β), p m → i ∉ m → p (m.insert i x)) (m : Map α β) : p m

@[simp]

theorem Map.fold_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_1} {f : γ → α → β → γ} {z : γ} {h : ∀ {acc : γ} {i : α} {x : β} {j : α} {y : β}, i ≠ j → f (f acc i x) j y = f (f acc j y) i x} : ∅.fold f z h = z

theorem Map.fold_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {γ : Type u_1} {f : γ → α → β → γ} {z : γ} {h : ∀ {acc : γ} {i : α} {x : β} {j : α} {y : β}, i ≠ j → f (f acc i x) j y = f (f acc j y) i x} {i : α} {x : β} (h₁ : i ∉ mp) : (mp.insert i x).fold f z h = mp.fold f (f z i x) ⋯

theorem Map.insert_comm {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} {j : α} {y : β} (h : i ≠ j ∨ x = y) : (mp.insert i x).insert j y = (mp.insert j y).insert i x

@[simp]

theorem Map.insert_idemp {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} : (mp.insert i x).insert i x = mp.insert i x

def Map.size {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) : ℕ

Equations

• mp.size = mp.inner.size

def Map.filter {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (p : α → β → Bool) : Map α β

Equations

• mp.filter p = { inner := Std.ExtDHashMap.filter p mp.inner }

def Map.count {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (p : α → β → Bool) : ℕ

Equations

• mp.count p = mp.inner.count p

@[simp]

theorem Map.size_filter_eq_count {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {p : α → β → Bool} : (mp.filter p).size = mp.count p

theorem Map.count_eq_size_filter {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {p : α → β → Bool} : mp.count p = (mp.filter p).size

@[simp]

theorem Map.count_le_size {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {p : α → β → Bool} : mp.count p ≤ mp.size

theorem Map.count_eq_zero_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {p : α → β → Bool} : mp.count p = 0 ↔ ∀ (i : α) (x : β), get? i mp = some x → ¬p i x = true

@[simp]

theorem Map.count_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : α → β → Bool} : ∅.count p = 0

theorem Map.count_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {p : α → β → Bool} {i : α} {x : β} (h : i ∉ mp) : (mp.insert i x).count p = mp.count p + if p i x = true then 1 else 0

def Map.push {α : Type u} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α ℕ) (i : α) : Map α ℕ

Equations

• mp.push i = mp.insert i ((Map.get? i mp).getD 0 + 1)

theorem Map.get?_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i j : α} {x : β} : get? i (mp.insert j x) = if j = i then some x else get? i mp

theorem Map.push_push_comm {α : Type u} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i j : α} {mp : Map α ℕ} : (mp.push i).push j = (mp.push j).push i

@[simp]

theorem Map.mem_push {α : Type u} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α ℕ} {x y : α} : y ∈ mp.push x ↔ y = x ∨ y ∈ mp

@[simp]

theorem Map.length_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.toList.length = mp.size

theorem Map.mem_iff_mem_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {k : α} : k ∈ mp ↔ k ∈ mp.keys

@[simp]

theorem Map.modifyMany_snoc {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {xs : List (α × (β → β))} {i : α} {f : β → β} : mp.modifyMany (xs ++ [(i, f)]) = (mp.modifyMany xs).modify i f

@[simp]

theorem Map.modify_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i : α} {f : β → β} : ∅.modify i f = ∅

@[simp]

theorem Map.mem_mk_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Std.ExtDHashMap α fun (x : α) => β} {i : α} : i ∈ { inner := mp } ↔ i ∈ mp

theorem Map.modify_of_notMem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {f : β → β} (h : i ∉ mp) : mp.modify i f = mp

theorem Map.modify_insert_of_ne {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} {j : α} {f : β → β} (h : i ≠ j) : (mp.insert i x).modify j f = (mp.modify j f).insert i x

@[simp]

theorem Map.toList_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {mp : Std.ExtDHashMap α fun (x : α) => β} : { inner := mp }.toList = List.map Sigma.toProd mp.toList

theorem Map.toList_insert_perm_cons_of_notMem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {x : β} (h : i ∉ mp) : (mp.insert i x).toList.Perm ((i, x) :: mp.toList)

theorem Map.values_insert_perm_of_notMem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {x : β} (h : i ∉ mp) : (mp.insert i x).values.Perm (x :: mp.values)

@[simp]

theorem Map.modify_insert_of_eq {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} {f : β → β} : (mp.insert i x).modify i f = mp.insert i (f x)

theorem Map.countP_values_modify_eq_of {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {p : β → Bool} {i : α} {f : β → β} (h : ∀ (x : β), p (f x) = p x) : List.countP p (mp.modify i f).values = List.countP p mp.values

theorem Map.countP_values_modifyMany_eq_of {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {p : β → Bool} {xs : List (α × (β → β))} (h : ∀ (k : α) (f : β → β) (x : β), (k, f) ∈ xs → p (f x) = p x) : List.countP p (mp.modifyMany xs).values = List.countP p mp.values

theorem Map.size_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} (h : i ∉ mp) : (mp.insert i x).size = mp.size + 1

@[simp]

theorem Map.size_modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {f : β → β} : (mp.modify i f).size = mp.size

theorem Map.get?_eq_some_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {x : β} : get? i mp = some x ↔ (i, x) ∈ mp.toList

@[simp]

theorem Map.nodup_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.keys.Nodup

@[simp]

theorem Map.mem_keys_iff_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {k : α} : k ∈ mp.keys ↔ k ∈ mp

@[simp]

theorem Map.length_keys {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.keys.length = mp.size

@[simp]

theorem Map.keys_modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {f : β → β} : (mp.modify i f).keys = mp.keys

def Map.erase {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : Map α β) (i : α) : Map α β

Equations

• mp.erase i = { inner := mp.inner.erase i }

@[simp]

theorem Map.mem_erase {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i j : α} : j ∈ mp.erase i ↔ j ≠ i ∧ j ∈ mp

@[simp]

theorem Map.pairwise_toList' {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : List.Pairwise (fun (x1 x2 : α × β) => x1.1 < x2.1) mp.toList

theorem Map.values_eq_map_snd_toList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] : mp.values = List.map (fun (x : α × β) => x.2) mp.toList

def Map.keyIdx {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : Map α β) (i : α) : ℕ

Equations

• mp.keyIdx i = List.idxOf i mp.keys

theorem Map.keyIdx_lt_size {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} (h : i ∈ mp) : mp.keyIdx i < mp.size

theorem Map.toList_modify_eq_list_modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {f : β → β} (h : i ∈ mp) : (mp.modify i f).toList = mp.toList.modify (mp.keyIdx i) fun (p : α × β) => (p.1, f p.2)

theorem Map.keyIdx_eq_of_toList_eq_append {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {x : β} {xs ys : List (α × β)} (h : mp.toList = xs ++ (i, x) :: ys) : mp.keyIdx i = xs.length

theorem Map.values_modify_eq_list_modify {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {f : β → β} (h : i ∈ mp) : (mp.modify i f).values = mp.values.modify (mp.keyIdx i) f

theorem Map.countP_values_modify_eq_ite_of_get? {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {p : β → Bool} {i : α} {x : β} {f : β → β} (h : get? i mp = some x) : List.countP p (mp.modify i f).values = (List.countP p mp.values + if p (f x) = true then 1 else 0) - if p x = true then 1 else 0

def Map.union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (m₁ m₂ : Map α β) : Map α β

Equations

• m₁.union m₂ = { inner := m₁.inner.union m₂.inner }

@[instance_reducible]

instance Map.instUnion {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : Union (Map α β)

Equations

• Map.instUnion = { union := Map.union }

theorem Map.union_def {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ ∪ m₂ = m₁.union m₂

@[simp]

theorem Map.inner_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : ∅.inner = ∅

@[simp]

theorem Map.inner_union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : (m₁ ∪ m₂).inner = m₁.inner ∪ m₂.inner

@[simp]

theorem Map.empty_union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} : ∅ ∪ mp = mp

@[simp]

theorem Map.union_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} : mp ∪ ∅ = mp

@[simp]

theorem Map.insertP_pair {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x : β} : insertP (i, x) mp = mp.insert i x

@[simp]

theorem Map.get?_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Std.ExtDHashMap α fun (x : α) => β} {i : α} : get? i { inner := mp } = mp.get? i

@[simp]

theorem Map.mk_union_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : Std.ExtDHashMap α fun (x : α) => β} : { inner := mp₁ } ∪ { inner := mp₂ } = { inner := mp₁ ∪ mp₂ }

theorem Map.get?_union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} : get? i (m₁ ∪ m₂) = (get? i m₂).or (get? i m₁)

@[simp]

theorem Map.inner_ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} : (ofList xs).inner = Std.ExtDHashMap.ofList (List.map Prod.toSigma xs)

@[simp]

theorem Map.ofList_singleton {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {x : α × β} : ofList [x] = insertP x ∅

@[simp]

theorem Map.insert_insert_same {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} {i : α} {x y : β} : (mp.insert i x).insert i y = mp.insert i y

theorem Map.insert_union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} {x : β} : (m₁ ∪ m₂).insert i x = m₁ ∪ m₂.insert i x

theorem Map.union_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} {x : β} : m₁ ∪ m₂.insert i x = (m₁ ∪ m₂).insert i x

@[simp]

theorem Map.ofList_append {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs ys : List (α × β)} : ofList (xs ++ ys) = ofList xs ∪ ofList ys

theorem Map.ofList_cons_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {x : α × β} {xs : List (α × β)} {y : β} (h : (x.1, y) ∈ xs) : ofList (x :: xs) = ofList xs

theorem Map.get?_union_left {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} (h : i ∉ m₂) : get? i (m₁ ∪ m₂) = get? i m₁

theorem Map.get?_union_right {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} (h : i ∉ m₁) : get? i (m₁ ∪ m₂) = get? i m₂

theorem Map.get!_union_left {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} [hb : Inhabited β] {i : α} (h : i ∉ m₂) : get! i (m₁ ∪ m₂) = get! i m₁

theorem Map.get!_union_right {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} [hb : Inhabited β] {i : α} (h : i ∉ m₁) : get! i (m₁ ∪ m₂) = get! i m₂

theorem Map.get!_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [hb : Inhabited β] {i : α} {x : β} {j : α} : get! j (mp.insert i x) = if j = i then x else get! j mp

theorem Map.get?_ofList_eq_some_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} {i : α} {x : β} (h : (List.map (fun (x : α × β) => x.1) xs).Nodup) : get? i (ofList xs) = some x ↔ (i, x) ∈ xs

theorem Map.get?_ofList_of_nodup {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} {i : α} (h : (List.map (fun (x : α × β) => x.1) xs).Nodup) : get? i (ofList xs) = Option.map (fun (x : α × β) => x.2) (List.find? (fun (x : α × β) => decide (x.1 = i)) xs)

theorem Map.get!_ofList_of_nodup {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hb : Inhabited β] {xs : List (α × β)} {i : α} (h : (List.map (fun (x : α × β) => x.1) xs).Nodup) : get! i (ofList xs) = (Option.map (fun (x : α × β) => x.2) (List.find? (fun (x : α × β) => decide (x.1 = i)) xs)).get!

@[simp]

theorem Map.mem_union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} : i ∈ m₁ ∪ m₂ ↔ i ∈ m₁ ∨ i ∈ m₂

@[simp]

theorem Map.keys_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {mp : Std.ExtDHashMap α fun (x : α) => β} : { inner := mp }.keys = mp.keys

@[simp]

theorem Map.insert_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Std.ExtDHashMap α fun (x : α) => β} {i : α} {x : β} : { inner := m }.insert i x = { inner := m.insert i x }

@[simp]

theorem Map.erase_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Std.ExtDHashMap α fun (x : α) => β} {i : α} : { inner := m }.erase i = { inner := m.erase i }

theorem Map.toList_insert_of_not_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Map α β} [ha : LinearOrder α] {i : α} {x : β} (h : i ∉ m) : (m.insert i x).toList = ((i, x) :: m.toList).mergeSort fun (x1 x2 : α × β) => decide (x1.1 ≤ x2.1)

theorem Map.keys_insert_of_not_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Map α β} [ha : LinearOrder α] {i : α} {x : β} (h : i ∉ m) : (m.insert i x).keys = (i :: m.keys).mergeSort fun (a b : α) => decide (a ≤ b)

@[simp]

theorem Map.insert_erase_eq_self_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Map α β} {i : α} {x : β} : (m.erase i).insert i x = m ↔ get? i m = some x

@[simp]

theorem Map.keys_eq_keys_iff {α : Type u} {β : Type v} {γ : Type w} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {m₁ : Map α β} {m₂ : Map α γ} : m₁.keys = m₂.keys ↔ ∀ (i : α), i ∈ m₁ ↔ i ∈ m₂

theorem Map.union_assoc {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ m₃ : Map α β} : m₁ ∪ m₂ ∪ m₃ = m₁ ∪ (m₂ ∪ m₃)

@[simp]

theorem Map.union_self {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Map α β} : m ∪ m = m

@[simp]

theorem Map.union_union_self {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ ∪ (m₁ ∪ m₂) = m₁ ∪ m₂

def Map.diff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (m₁ m₂ : Map α β) : Map α β

Equations

• m₁.diff m₂ = { inner := m₁.inner \ m₂.inner }

@[instance_reducible]

instance Map.instSDiff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : SDiff (Map α β)

Equations

• Map.instSDiff = { sdiff := Map.diff }

theorem Map.diff_def {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ \ m₂ = m₁.diff m₂

@[simp]

theorem Map.mk_diff_mk {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Std.ExtDHashMap α fun (x : α) => β} : { inner := m₁ } \ { inner := m₂ } = { inner := m₁ \ m₂ }

theorem Map.get?_diff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} : get? i (m₁ \ m₂) = if i ∈ m₂ then none else get? i m₁

@[simp]

theorem Map.union_diff_self {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ ∪ m₂ \ m₁ = m₂ ∪ m₁

theorem Map.union_eq_self_left_iff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} : m₁ ∪ m₂ = m₁ ↔ ∀ (i : α) (x : β), get? i m₂ = some x → get? i m₁ = some x

@[simp]

theorem Map.union_insert_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ : Map α β} {i : α} {x : β} : m₁ ∪ ∅.insert i x = m₁.insert i x

theorem Map.toList_ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List (α × β)} (h : (List.map (fun (x : α × β) => x.1) xs).Nodup) : (ofList xs).toList = xs.mergeSort fun (x1 x2 : α × β) => decide (x1.1 ≤ x2.1)

theorem Map.union_eq_union_iff_right {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m m₁ m₂ : Map α β} (h₁ : ∀ i ∈ m, i ∉ m₁) (h₂ : ∀ i ∈ m, i ∉ m₂) : m ∪ m₁ = m ∪ m₂ ↔ m₁ = m₂

theorem Map.get?_union_ite {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} : get? i (m₁ ∪ m₂) = if i ∈ m₂ then get? i m₂ else get? i m₁

@[simp]

theorem Map.mem_diff {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} {i : α} : i ∈ m₁ \ m₂ ↔ i ∈ m₁ ∧ i ∉ m₂

theorem Map.toList_ofList_subset {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List (α × β)} : (ofList xs).toList ⊆ xs

theorem Map.mem_of_mem_toList_ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List (α × β)} {p : α × β} (h : p ∈ (ofList xs).toList) : p ∈ xs

theorem Map.mem_of_get?_ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} {i : α} {x : β} (h : get? i (ofList xs) = some x) : (i, x) ∈ xs

@[simp]

theorem Map.get!_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hb : Inhabited β] {i : α} : get! i ∅ = default

@[simp]

theorem Map.insert_empty_eq_insert_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i j : α} {x y : β} : ∅.insert i x = ∅.insert j y ↔ i = j ∧ x = y

theorem Map.ofList_eq_foldl {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} : ofList xs = List.foldl (fun (m : Map α β) (x : α × β) => insertP x m) ∅ xs

theorem Map.keys_insert_of_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {x : β} (h : i ∈ mp) : (mp.insert i x).keys = mp.keys

theorem Map.keys_insert {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : Map α β} [ha : LinearOrder α] {i : α} {x : β} : (mp.insert i x).keys = if i ∈ mp then mp.keys else (i :: mp.keys).mergeSort fun (a b : α) => decide (a ≤ b)

@[simp]

theorem Map.keys_empty {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] : ∅.keys = []

theorem Map.get?_ofList_of_nodup_and_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List (α × β)} {i : α} {x : β} (h₁ : (List.map (fun (x : α × β) => x.1) xs).Nodup) (h₂ : (i, x) ∈ xs) : get? i (ofList xs) = some x

theorem Map.get!_ofList_of_nodup_and_mem {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hb : Inhabited β] {xs : List (α × β)} {i : α} {x : β} (h₁ : (List.map (fun (x : α × β) => x.1) xs).Nodup) (h₂ : (i, x) ∈ xs) : get! i (ofList xs) = x

theorem Map.keys_union {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : Map α β} [ha : LinearOrder α] (h : ∀ i ∈ m₁, i ∉ m₂) : (m₁ ∪ m₂).keys = (m₁.keys ++ m₂.keys).mergeSort fun (a b : α) => decide (a ≤ b)

theorem Map.keys_ofList {α : Type u} {β : Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List (α × β)} (h : (List.map (fun (x : α × β) => x.1) xs).Nodup) : (ofList xs).keys = (List.map (fun (x : α × β) => x.1) xs).mergeSort fun (a b : α) => decide (a ≤ b)