Projects.Util.ExtDHashMap

@[simp]

theorem Std.ExtDHashMap.not_mem_empty' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i : α} :

i ∉ ∅

source

@[simp]

theorem Std.ExtDHashMap.not_mem_lift_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {i : α} :

i ∉ { inner := ⟦∅⟧ }

source

theorem Std.ExtDHashMap.mem_iff_get?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} :

i ∈ mp ↔ ∃ (x : β i), mp.get? i = some x

source

theorem Std.ExtDHashMap.get?_eq_some_of_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} (h : i ∈ mp) :

∃ (x : β i), mp.get? i = some x

source

theorem Std.ExtDHashMap.get?_eq_none_of_not_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} (h : i ∉ mp) :

mp.get? i = none

source

@[simp]

theorem Std.ExtDHashMap.get?_eq_none_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} :

mp.get? i = none ↔ i ∉ mp

source

def Std.ExtDHashMap.toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : ExtDHashMap α β) :

List ((i : α) × β i)

Equations

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

Instances For

source

@[simp]

theorem Std.ExtDHashMap.toList_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] :

∅.toList = []

source

@[simp]

theorem Std.ExtDHashMap.ofList_snoc {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((a : α) × β a)} {x : (i : α) × β i} :

ofList (xs ++ [x]) = Insert.insert x (ofList xs)

source

@[simp]

theorem Std.ExtDHashMap.mem_insert' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {x : (i : α) × β i} {i : α} :

i ∈ Insert.insert x mp ↔ i = x.fst ∨ i ∈ mp

source

@[simp]

theorem Std.ExtDHashMap.mem_ofList' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((i : α) × β i)} {i : α} :

i ∈ ofList xs ↔ ∃ (x : β i), ⟨i, x⟩ ∈ xs

source

theorem Std.ExtDHashMap.eq_empty_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} :

mp = ∅ ↔ ∀ (i : α), i ∉ mp

source

theorem Std.ExtDHashMap.ext_iff' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : ExtDHashMap α β} :

m₁ = m₂ ↔ m₁.inner.out.Equiv m₂.inner.out

source

theorem Std.ExtDHashMap.ext_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : ExtDHashMap α β} :

m₁ = m₂ ↔ ∀ (i : α), m₁.get? i = m₂.get? i

source

theorem Std.ExtDHashMap.get?_eq_ite_of_unit {α : Type u_1} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : ExtDHashMap α fun (x : α) => Unit} {i : α} :

m.get? i = if i ∈ m then some () else none

source

theorem Std.ExtDHashMap.ofList_eq_ofList_iff {α : Type u_1} {β : α → Type u_2} [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

source

def Std.ExtDHashMap.range' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] (f : (i : α) → Option (β i)) :

ExtDHashMap α β

Equations

Std.ExtDHashMap.range' f = Quotient.liftWith Fintype.elems.val (fun (xs : List α) => Std.ExtDHashMap.ofList (List.filterMap (fun (i : α) => Option.map (fun (x : β i) => ⟨i, x⟩) (f i)) xs)) ⋯

Instances For

source

def Std.ExtDHashMap.range {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] (f : (i : α) → β i) :

ExtDHashMap α β

Equations

Std.ExtDHashMap.range f = Quotient.liftWith Fintype.elems.val (fun (xs : List α) => Std.ExtDHashMap.ofList (List.map (fun (i : α) => ⟨i, f i⟩) xs)) ⋯

Instances For

source

@[simp]

theorem Std.ExtDHashMap.mem_range {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f : (i : α) → β i} {i : α} :

i ∈ range f

source

@[simp]

theorem Std.ExtDHashMap.mem_range' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f : (i : α) → Option (β i)} {i : α} :

i ∈ range' f ↔ ∃ (x : β i), f i = some x

source

@[simp]

theorem Std.ExtDHashMap.nonempty_insert {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {x : (a : α) × β a} :

Insert.insert x mp ≠ { inner := ⟦∅⟧ }

source

@[simp]

theorem Std.ExtDHashMap.nodup_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [LinearOrder α] :

mp.toList.Nodup

source

@[simp]

theorem Std.ExtDHashMap.pairwise_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [LinearOrder α] :

List.Pairwise (fun (x1 x2 : (i : α) × β i) => x1.fst ≤ x2.fst) mp.toList

source

@[simp]

theorem Std.ExtDHashMap.mem_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {x : (i : α) × β i} [LinearOrder α] :

x ∈ mp.toList ↔ mp.get? x.fst = some x.snd

source

@[simp]

theorem Std.ExtDHashMap.toList_eq_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] {m₁ m₂ : ExtDHashMap α β} :

m₁.toList = m₂.toList ↔ m₁ = m₂

source

@[simp]

theorem Std.ExtDHashMap.toList_eq_nil_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [LinearOrder α] :

mp.toList = [] ↔ mp = ∅

source

theorem Std.ExtDHashMap.eq_iff_inner_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : ExtDHashMap α β} :

m₁ = m₂ ↔ m₁.inner = m₂.inner

source

theorem Std.ExtDHashMap.inner_eq_iff_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m₁ m₂ : ExtDHashMap α β} :

m₁.inner = m₂.inner ↔ m₁ = m₂

source

def Std.ExtDHashMap.fold {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} (mp : ExtDHashMap α β) (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 = Std.ExtDHashMap.lift (fun (x : Std.DHashMap α β) => Std.DHashMap.fold f z x) ⋯ mp

Instances For

source

def Std.ExtDHashMap.decideEq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : (i : α) → DecidableEq (β i)] (m₁ m₂ : ExtDHashMap α β) :

Bool

Equations

m₁.decideEq m₂ = Std.ExtDHashMap.casesOn m₁ fun (m₁ : Quotient (Std.DHashMap.isSetoid α β)) => Std.ExtDHashMap.casesOn m₂ fun (m₂ : Quotient (Std.DHashMap.isSetoid α β)) => m₁.liftOn₂ m₂ Std.DHashMap.decideEquiv ⋯

Instances For

source

theorem Std.ExtDHashMap.eq_iff_decideEq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : (i : α) → DecidableEq (β i)] {m₁ m₂ : ExtDHashMap α β} :

m₁ = m₂ ↔ m₁.decideEq m₂ = true

source

@[instance_reducible]

instance Std.ExtDHashMap.instDecidableEq_projects {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : (i : α) → DecidableEq (β i)] :

DecidableEq (ExtDHashMap α β)

Equations

m₁.instDecidableEq_projects m₂ = match h : m₁.decideEq m₂ with | true => isTrue ⋯ | false => isFalse ⋯

source

@[simp]

theorem Std.ExtDHashMap.decideEq_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [hh : (i : α) → DecidableEq (β i)] {m₁ m₂ : ExtDHashMap α β} :

m₁.decideEq m₂ = decide (m₁ = m₂)

source

def Std.ExtDHashMap.all {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : ExtDHashMap α β) (p : (i : α) → β i → Bool) :

Bool

Equations

mp.all p = Quotient.lift (fun (x : Std.DHashMap α β) => x.all p) ⋯ mp.inner

Instances For

source

@[simp]

theorem Std.ExtDHashMap.all_def {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {p : (i : α) → β i → Bool} [LinearOrder α] :

mp.all p = decide (∀ x ∈ mp.toList, p x.fst x.snd = true)

source

def Std.ExtDHashMap.keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : ExtDHashMap α β) :

List α

Equations

mp.keys = Std.ExtDHashMap.lift Std.DHashMap.toSortedKeys ⋯ mp

Instances For

source

@[simp]

theorem Std.ExtDHashMap.mem_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [LinearOrder α] {i : α} :

i ∈ mp.keys ↔ i ∈ mp

source

def Std.ExtDHashMap.modifyMany {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : ExtDHashMap α β) (xs : List ((i : α) × (β i → β i))) :

ExtDHashMap α β

Equations

mp.modifyMany xs = { inner := Quotient.map (fun (x : Std.DHashMap α β) => x.modifyMany xs) ⋯ mp.inner }

Instances For

source

@[simp]

theorem Std.ExtDHashMap.modifyMany_nil {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} :

mp.modifyMany [] = mp

source

@[simp]

theorem Std.ExtDHashMap.modifyMany_cons {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} {x : β i → β i} {xs : List ((i : α) × (β i → β i))} :

mp.modifyMany (⟨i, x⟩ :: xs) = (mp.modify i x).modifyMany xs

source

theorem Std.ExtDHashMap.get!_eq_get? {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} [hb : Inhabited (β i)] :

mp.get! i = (mp.get? i).get!

source

theorem Std.ExtDHashMap.get?_eq_ite {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} [hb : Inhabited (β i)] :

mp.get? i = if i ∈ mp then some (mp.get! i) else none

source

theorem Std.ExtDHashMap.get?_ofList_eq_some_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((i : α) × β i)} {i : α} {x : β i} (h : (List.map (fun (x : (i : α) × β i) => x.fst) xs).Nodup) :

(ofList xs).get? i = some x ↔ ⟨i, x⟩ ∈ xs

source

@[simp]

theorem Std.ExtDHashMap.get?_range {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f : (i : α) → β i} {i : α} :

(range f).get? i = some (f i)

source

@[simp]

theorem Std.ExtDHashMap.get?_range' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f : (i : α) → Option (β i)} {i : α} :

(range' f).get? i = f i

source

theorem Std.ExtDHashMap.injective_range {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] :

Function.Injective range

source

theorem Std.ExtDHashMap.injective_range' {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] :

Function.Injective range'

source

@[instance_reducible]

instance Std.ExtDHashMap.instFintype_projects {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] [hb : (i : α) → Fintype (β i)] :

Fintype (ExtDHashMap α β)

Equations

Std.ExtDHashMap.instFintype_projects = { elems := Finset.map { toFun := Std.ExtDHashMap.range', inj' := ⋯ } Fintype.elems, complete := ⋯ }

source

instance Std.ExtDHashMap.instFinite_projects {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Finite α] [hb : ∀ (i : α), Finite (β i)] :

Finite (ExtDHashMap α β)

source

@[simp]

theorem Std.ExtDHashMap.range_eq_range_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f g : (i : α) → β i} :

range f = range g ↔ ∀ (x : α), f x = g x

source

@[simp]

theorem Std.ExtDHashMap.range'_eq_range'_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : Fintype α] {f g : (i : α) → Option (β i)} :

range' f = range' g ↔ ∀ (x : α), f x = g x

source

theorem Std.ExtDHashMap.mem_of_get?_eq_some {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} {x : β i} (h : mp.get? i = some x) :

i ∈ mp

source

@[simp]

theorem Std.ExtDHashMap.get?_eq_some_get!_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} [hb : Inhabited (β i)] :

mp.get? i = some (mp.get! i) ↔ i ∈ mp

source

@[simp]

theorem Std.ExtDHashMap.get?_eq_some_get?_get! {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} [hb : Inhabited (β i)] :

mp.get? i = some (mp.get? i).get! ↔ i ∈ mp

source

theorem Std.ExtDHashMap.fold_eq_foldl_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {γ : Type u_4} {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

source

theorem Std.ExtDHashMap.eq_iff_toList_eq {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {m₁ m₂ : ExtDHashMap α β} :

m₁ = m₂ ↔ m₁.toList = m₂.toList

source

@[simp]

theorem Std.ExtDHashMap.ofList_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

ofList mp.toList = mp

source

theorem Std.ExtDHashMap.toList_ofList_perm {α : Type u_1} {β : α → Type u_2} [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

source

@[simp]

theorem Std.ExtDHashMap.sortedLE_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.keys.SortedLE

source

theorem Std.ExtDHashMap.keys_eq_map_fst_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.keys = List.map (fun (x : (i : α) × β i) => x.fst) mp.toList

source

def Std.ExtDHashMap.minKey? {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : ExtDHashMap α β) :

Option α

Equations

mp.minKey? = mp.fold (fun (acc : Option α) (i : α) (x : β i) => some (acc.elim i fun (acc : α) => min acc i)) none ⋯

Instances For

source

def Std.ExtDHashMap.maxKey? {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] (mp : ExtDHashMap α β) :

Option α

Equations

mp.maxKey? = mp.fold (fun (acc : Option α) (i : α) (x : β i) => some (acc.elim i fun (acc : α) => max acc i)) none ⋯

Instances For

source

def Std.ExtDHashMap.minKey! {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (mp : ExtDHashMap α β) :

Equations

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

Instances For

source

def Std.ExtDHashMap.maxKey! {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] [Inhabited α] (mp : ExtDHashMap α β) :

Equations

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

Instances For

source

theorem Std.ExtDHashMap.minKey?_eq_head?_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.minKey? = mp.keys.head?

source

theorem Std.ExtDHashMap.maxKey?_eq_getLast?_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.maxKey? = mp.keys.getLast?

source

@[simp]

theorem Std.ExtDHashMap.minKey?_eq_none_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.minKey? = none ↔ mp = ∅

source

@[simp]

theorem Std.ExtDHashMap.maxKey?_eq_none_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.maxKey? = none ↔ mp = ∅

source

theorem Std.ExtDHashMap.not_mem_of_lt_minKey? {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.minKey? = some m) (h₂ : x < m) :

x ∉ mp

source

theorem Std.ExtDHashMap.not_mem_of_maxKey?_lt {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.maxKey? = some m) (h₂ : m < x) :

x ∉ mp

source

theorem Std.ExtDHashMap.not_mem_of_lt_minKey! {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : x < mp.minKey!) :

x ∉ mp

source

theorem Std.ExtDHashMap.not_mem_of_maxKey!_lt {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : mp.maxKey! < x) :

x ∉ mp

source

theorem Std.ExtDHashMap.minKey?_le_of_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.minKey? = some m) (h₂ : x ∈ mp) :

m ≤ x

source

theorem Std.ExtDHashMap.le_maxKey?_of_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {m x : α} (h₁ : mp.maxKey? = some m) (h₂ : x ∈ mp) :

x ≤ m

source

theorem Std.ExtDHashMap.minKey!_le_of_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : x ∈ mp) :

mp.minKey! ≤ x

source

theorem Std.ExtDHashMap.le_maxKey!_of_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha₁ : Inhabited α] [ha₂ : LinearOrder α] {x : α} (h : x ∈ mp) :

x ≤ mp.maxKey!

source

@[simp]

theorem Std.ExtDHashMap.keys_eq_nil_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [LinearOrder α] :

mp.keys = [] ↔ mp.isEmpty = true

source

@[simp]

theorem Std.ExtDHashMap.keys_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [LinearOrder α] :

∅.keys = []

source

theorem Std.ExtDHashMap.ind {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : ExtDHashMap α β → Prop} (h₁ : p ∅) (h₂ : ∀ (mp : ExtDHashMap α β) (i : α) (x : β i), i ∉ mp → p mp → p (mp.insert i x)) (mp : ExtDHashMap α β) :

p mp

source

@[simp]

theorem Std.ExtDHashMap.fold_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {γ : Type u_4} {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

source

theorem Std.ExtDHashMap.fold_insert {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {γ : Type u_4} {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) ⋯

source

theorem Std.ExtDHashMap.insert_comm {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {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

source

@[simp]

theorem Std.ExtDHashMap.insert_idemp {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} {x : β i} :

(mp.insert i x).insert i x = mp.insert i x

source

def Std.ExtDHashMap.count {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] (mp : ExtDHashMap α β) (p : (i : α) → β i → Bool) :

ℕ

Equations

mp.count p = Quotient.lift (fun (x : Std.DHashMap α β) => x.count p) ⋯ mp.inner

Instances For

source

@[simp]

theorem Std.ExtDHashMap.size_filter_eq_count {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {p : (a : α) → β a → Bool} :

(filter p mp).size = mp.count p

source

theorem Std.ExtDHashMap.count_eq_size_filter {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {p : (i : α) → β i → Bool} :

mp.count p = (filter p mp).size

source

@[simp]

theorem Std.ExtDHashMap.count_le_size {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {p : (i : α) → β i → Bool} :

mp.count p ≤ mp.size

source

theorem Std.ExtDHashMap.count_eq_zero_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {p : (i : α) → β i → Bool} :

mp.count p = 0 ↔ ∀ (i : α) (x : β i), mp.get? i = some x → ¬p i x = true

source

@[simp]

theorem Std.ExtDHashMap.count_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {p : (i : α) → β i → Bool} :

∅.count p = 0

source

theorem Std.ExtDHashMap.count_insert {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {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

source

theorem Std.ExtDHashMap.eq_iff_inner {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : ExtDHashMap α β} :

mp₁ = mp₂ ↔ mp₁.inner = mp₂.inner

source

@[simp]

theorem Std.ExtDHashMap.mem_mk_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} {i : α} :

i ∈ { inner := ⟦mp⟧ } ↔ i ∈ mp

source

theorem Std.ExtDHashMap.modify_of_notMem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} {i : α} {f : β i → β i} (h : i ∉ mp) :

mp.modify i f = mp

source

theorem Std.ExtDHashMap.toList_insert_perm_cons_of_notMem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {i : α} {x : β i} (h : i ∉ mp) :

(mp.insert i x).toList.Perm (⟨i, x⟩ :: mp.toList)

source

@[simp]

theorem Std.ExtDHashMap.nodup_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.keys.Nodup

source

@[simp]

theorem Std.ExtDHashMap.sortedLT_keys {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] :

mp.keys.SortedLT

source

theorem Std.ExtDHashMap.union_def {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp₁ mp₂ : ExtDHashMap α β} :

mp₁ ∪ mp₂ = mp₁.union mp₂

source

@[simp]

theorem Std.ExtDHashMap.get?_out_mk {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : DHashMap α β} :

⟦mp⟧.out.get? = mp.get?

source

@[simp]

theorem Std.ExtDHashMap.empty_union {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} :

∅ ∪ mp = mp

source

@[simp]

theorem Std.ExtDHashMap.union_empty {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} :

mp ∪ ∅ = mp

source

theorem Std.ExtDHashMap.toList_insert_of_not_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : ExtDHashMap α β} [ha : LinearOrder α] {i : α} {x : β i} (h : i ∉ m) :

(m.insert i x).toList = (⟨i, x⟩ :: m.toList).mergeSort fun (x1 x2 : (i : α) × β i) => decide (x1.fst ≤ x2.fst)

source

theorem Std.ExtDHashMap.keys_insert_of_not_mem {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : ExtDHashMap α β} [ha : LinearOrder α] {i : α} {x : β i} (h : i ∉ m) :

(m.insert i x).keys = (i :: m.keys).mergeSort fun (a b : α) => decide (a ≤ b)

source

@[simp]

theorem Std.ExtDHashMap.get?_out_inner {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : ExtDHashMap α β} {i : α} :

m.inner.out.get? i = m.get? i

source

@[simp]

theorem Std.ExtDHashMap.get?_mk {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Quotient (DHashMap.isSetoid α β)} {i : α} :

{ inner := m }.get? i = m.out.get? i

source

@[simp]

theorem Std.ExtDHashMap.insert_mk {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Quotient (DHashMap.isSetoid α β)} {i : α} {x : β i} :

{ inner := m }.insert i x = { inner := ⟦m.out.insert i x⟧ }

source

@[simp]

theorem Std.ExtDHashMap.erase_mk {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : Quotient (DHashMap.isSetoid α β)} {i : α} :

{ inner := m }.erase i = { inner := ⟦m.out.erase i⟧ }

source

@[simp]

theorem Std.ExtDHashMap.insert_erase_eq_self_iff {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m : ExtDHashMap α β} {i : α} {x : β i} :

(m.erase i).insert i x = m ↔ m.get? i = some x

source

@[simp]

theorem Std.ExtDHashMap.keys_eq_keys_iff {α : Type u_1} {β : α → Type u_2} {γ : α → Type u_3} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {m₁ : ExtDHashMap α β} {m₂ : ExtDHashMap α γ} :

m₁.keys = m₂.keys ↔ ∀ (i : α), i ∈ m₁ ↔ i ∈ m₂

source

theorem Std.ExtDHashMap.toList_ofList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List ((i : α) × β i)} (h : (List.map (fun (x : (i : α) × β i) => x.fst) xs).Nodup) :

(ofList xs).toList = xs.mergeSort fun (x1 x2 : (i : α) × β i) => decide (x1.fst ≤ x2.fst)

source

theorem Std.ExtDHashMap.union_eq_union_iff_right {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {m m₁ m₂ : ExtDHashMap α β} (h₁ : ∀ i ∈ m, i ∉ m₁) (h₂ : ∀ i ∈ m, i ∉ m₂) :

m ∪ m₁ = m ∪ m₂ ↔ m₁ = m₂

source

theorem Std.ExtDHashMap.get?_eq_some_iff_mem_toList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {mp : ExtDHashMap α β} [ha : LinearOrder α] {i : α} {x : β i} :

mp.get? i = some x ↔ ⟨i, x⟩ ∈ mp.toList

source

theorem Std.ExtDHashMap.toList_ofList_subset {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List ((i : α) × β i)} :

(ofList xs).toList ⊆ xs

source

theorem Std.ExtDHashMap.mem_of_mem_toList_ofList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] [ha : LinearOrder α] {xs : List ((i : α) × β i)} {p : (i : α) × β i} (h : p ∈ (ofList xs).toList) :

p ∈ xs

source

theorem Std.ExtDHashMap.mem_of_get?_ofList {α : Type u_1} {β : α → Type u_2} [hh₁ : DecidableEq α] [hh₂ : Hashable α] {xs : List ((i : α) × β i)} {i : α} {x : β i} (h : (ofList xs).get? i = some x) :

⟨i, x⟩ ∈ xs