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

• inner : Std.ExtDHashMap α β

@[instance_reducible]

instance instInhabitedDMap {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} {a✝² : DecidableEq a✝} {a✝³ : Hashable a✝} : Inhabited (DMap a✝ a✝¹)

Equations

• instInhabitedDMap = { default := instInhabitedDMap.default }

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

Equations

• DMap.empty = { inner := ∅ }

@[instance_reducible]

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

Equations

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

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

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

Equations

• DMap.insertP x mp = { inner := insert x mp.inner }

@[instance_reducible]

instance DMap.instInsertSigma {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] : Insert ((i : α) × β i) (DMap α β)

Equations

• DMap.instInsertSigma = { insert := DMap.insertP }

theorem DMap.insert_def {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {x : (i : α) × β i} {mp : DMap α β} : insert x mp = { inner := insert x mp.inner }

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

Equations

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

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

Equations

• DMap.ofList xs = { inner := Std.ExtDHashMap.ofList xs }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

@[instance_reducible]

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

Equations

• DMap.instDecidableMem = id inferInstance

@[instance_reducible]

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

Equations

• DMap.instDecidableMem_1 = id inferInstance

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

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

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

@[simp]

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

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

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

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

Equations

• mp.toList = Std.ExtDHashMap.lift Std.DHashMap.toSortedList ⋯ mp.inner

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem DMap.mem_insertP {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DMap α β} {x : (i : α) × β i} {i : α} : i ∈ insertP x mp ↔ i = x.fst ∨ i ∈ mp

@[simp]

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

@[simp]

theorem DMap.mem_insert {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DMap α β} {x : (i : α) × β i} {i : α} : i ∈ insert x mp ↔ i = x.fst ∨ i ∈ mp

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem DMap.mem_toList {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DMap α β} [LinearOrder α] {x : (i : α) × β i} : x ∈ mp.toList ↔ get? x.fst mp = some x.snd

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

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

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

Equations

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

@[simp]

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

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

Equations

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

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

Equations

• mp.modifyMany xs = { inner := mp.inner.modifyMany xs }

@[simp]

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

@[simp]

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

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

Equations

• mp.insertMany xs = { inner := mp.inner.insertMany xs }

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[instance_reducible]

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

Equations

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

instance DMap.instFinite {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Finite α] [hb : ∀ (i : α), Finite (β i)] : Finite (DMap α β)

@[simp]

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

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

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

@[simp]

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

@[simp]

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

def DMap.fold {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_1} (mp : DMap α β) (f : γ → (i : α) → β i → γ) (z : γ) (h_assoc : ∀ {acc : γ} {i : α} {x : β i} {j : α} {y : β j}, 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 DMap.fold_eq_foldl_toList {α : Type u} {β : α → Type v} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DMap α β} [ha : LinearOrder α] {γ : Type u_1} {z : γ} {f : γ → (i : α) → β i → γ} {h_assoc : ∀ {acc : γ} {i : α} {x : β i} {j : α} {y : β j}, 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 : (i : α) × β i) => f acc x.fst x.snd) z mp.toList

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

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

@[simp]

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

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

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

Equations

• mp.keys = mp.inner.keys

@[simp]

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

@[simp]

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

Equations

• mp.size = mp.inner.size

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

Equations

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

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

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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