Dependent tree map lemmas #
This file contains lemmas about Std.DTreeMap. Most of the lemmas require
TransCmp cmp for the comparison function cmp.
theorem Std.DTreeMap.toArray_insert_perm {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.Const.toList_insert_perm {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
theorem Std.DTreeMap.Const.toArray_insert_perm {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
@[simp]
theorem Std.DTreeMap.getD_emptyc {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
theorem Std.DTreeMap.getD_insert {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
theorem Std.DTreeMap.mem_of_mem_insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t
theorem Std.DTreeMap.mem_of_mem_insertIfNew' {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ ¬k ∈ t) → a ∈ t
This is a restatement of mem_of_mem_insertIfNew that is written to exactly match the
proof obligation in the statement of get_insertIfNew.
theorem Std.DTreeMap.get?_insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} :
theorem Std.DTreeMap.get_insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v} :
theorem Std.DTreeMap.get!_insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
theorem Std.DTreeMap.getD_insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
(t.insertIfNew k v).getD a fallback = if h : cmp k a = Ordering.eq ∧ ¬k ∈ t then cast ⋯ v else t.getD a fallback
theorem Std.DTreeMap.Const.get_insertIfNew {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v} :
theorem Std.DTreeMap.getKey_insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v} :
@[simp]
theorem Std.DTreeMap.getThenInsertIfNew?_fst {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.getThenInsertIfNew?_snd {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.distinct_keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.keys
theorem Std.DTreeMap.ordered_keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.keys
theorem Std.DTreeMap.find?_toList_eq_some_iff_get?_eq_some {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.find?_toArray_eq_some_iff_get?_eq_some {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.distinct_keys_toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) t.toList
theorem Std.DTreeMap.ordered_keys_toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : (a : α) × β a) => cmp a.fst b.fst = Ordering.lt) t.toList
theorem Std.DTreeMap.Const.distinct_keys_toList {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) (toList t)
theorem Std.DTreeMap.Const.ordered_keys_toList {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α × β) => cmp a.fst b.fst = Ordering.lt) (toList t)
theorem Std.DTreeMap.foldlM_eq_foldlM_toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} :
theorem Std.DTreeMap.foldlM_eq_foldlM_toArray {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} :
theorem Std.DTreeMap.foldrM_eq_foldrM_toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
theorem Std.DTreeMap.foldrM_eq_foldrM_toArray {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
@[simp]
theorem Std.DTreeMap.forIn_toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (c : DTreeMap α β cmp) :
instance Std.DTreeMap.instPureForInSigmaOfLawfulMonad {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w'} [Monad m] [LawfulMonad m] :
Internal.PureForIn m (DTreeMap α β cmp) ((a : α) × β a)
theorem Std.DTreeMap.foldlM_eq_foldlM_keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
theorem Std.DTreeMap.foldlM_eq_foldlM_keysArray {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
theorem Std.DTreeMap.foldrM_eq_foldrM_keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
theorem Std.DTreeMap.foldrM_eq_foldrM_keysArray {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Const.foldlM_eq_foldlM_toList {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
theorem Std.DTreeMap.Const.foldlM_eq_foldlM_toArray {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
theorem Std.DTreeMap.Const.foldrM_eq_foldrM_toList {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
theorem Std.DTreeMap.Const.foldrM_eq_foldrM_toArray {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
@[simp]
theorem Std.DTreeMap.insertMany_nil {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} :
theorem Std.DTreeMap.get?_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.get?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.get_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l} :
theorem Std.DTreeMap.get_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) {h' : k' ∈ t.insertMany l} :
theorem Std.DTreeMap.get!_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.get!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.getD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.getKey?_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l} :
theorem Std.DTreeMap.getKey_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) {h' : k' ∈ t.insertMany l} :
theorem Std.DTreeMap.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.getKey!_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.getKeyD_insertMany_list_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.size_insertMany_list {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) :
@[simp]
theorem Std.DTreeMap.Const.insertMany_nil {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} :
@[simp]
theorem Std.DTreeMap.Const.getKey?_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ insertMany t l} :
theorem Std.DTreeMap.Const.getKey_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) {h' : k' ∈ insertMany t l} :
theorem Std.DTreeMap.Const.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.getKey!_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Const.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.getKeyD_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Const.size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) :
theorem Std.DTreeMap.Const.get?_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Const.get?_insertMany_list {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
theorem Std.DTreeMap.Const.get_insertMany_list_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ insertMany t l} :
theorem Std.DTreeMap.Const.get_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) {h' : k' ∈ insertMany t l} :
theorem Std.DTreeMap.Const.get!_insertMany_list_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited β] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.get!_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Const.getD_insertMany_list_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.getD_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
@[simp]
theorem Std.DTreeMap.Const.insertManyIfNewUnit_nil {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} :
@[simp]
theorem Std.DTreeMap.Const.insertManyIfNewUnit_list_singleton {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {k : α} :
theorem Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit t l).getKey? k' = some k
theorem Std.DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k : α} {h' : k ∈ insertManyIfNewUnit t l} (contains : k ∈ t) :
theorem Std.DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {h' : k' ∈ insertManyIfNewUnit t l} :
¬k ∈ t → List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit t l).getKey k' h' = k
theorem Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) :
¬k ∈ t → List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit t l).getKey! k' = k
theorem Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} :
theorem Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) :
¬k ∈ t →
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l → k ∈ l → (insertManyIfNewUnit t l).getKeyD k' fallback = k
theorem Std.DTreeMap.Const.size_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) :
@[simp]
@[simp]
theorem Std.DTreeMap.Const.get_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {l : List α} {k : α} {h' : k ∈ insertManyIfNewUnit t l} :
theorem Std.DTreeMap.ofList_eq_insertMany_empty {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {l : List ((a : α) × β a)} :
theorem Std.DTreeMap.get?_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.get_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) {h : k' ∈ ofList l cmp} :
theorem Std.DTreeMap.get!_ofList_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.get!_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.getD_ofList_of_contains_eq_false {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.getD_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : ⟨k, v⟩ ∈ l) :
theorem Std.DTreeMap.getKey?_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.getKey_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) {h' : k' ∈ ofList l cmp} :
theorem Std.DTreeMap.getKey!_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.getKeyD_ofList_of_mem {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Sigma.fst l) :
theorem Std.DTreeMap.Const.get?_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Const.get_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) {h : k' ∈ ofList l cmp} :
theorem Std.DTreeMap.Const.getD_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) ∈ l) :
theorem Std.DTreeMap.Const.getKey?_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Const.getKey_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) {h' : k' ∈ ofList l cmp} :
theorem Std.DTreeMap.Const.getKey!_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] [Inhabited α] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
theorem Std.DTreeMap.Const.getKeyD_ofList_of_mem {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k ∈ List.map Prod.fst l) :
@[simp]
@[simp]
theorem Std.DTreeMap.Const.unitOfList_cons {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α} :
theorem Std.DTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty {α : Type u} {cmp : α → α → Ordering} {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.contains_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.mem_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey?_unitOfList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.DTreeMap.Const.getKey?_unitOfList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
theorem Std.DTreeMap.Const.getKey_unitOfList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) {h' : k' ∈ unitOfList l cmp} :
theorem Std.DTreeMap.Const.getKey!_unitOfList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
theorem Std.DTreeMap.Const.getKeyD_unitOfList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :
theorem Std.DTreeMap.Const.getKeyD_unitOfList_of_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) :
theorem Std.DTreeMap.Const.size_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) :
theorem Std.DTreeMap.Const.size_unitOfList_le {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.isEmpty_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.get_unitOfList {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {h : k ∈ unitOfList l cmp} :
@[simp]
theorem Std.DTreeMap.Const.get!_unitOfList {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} :
theorem Std.DTreeMap.size_alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.get!_alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} [Inhabited (β k')] {f : Option (β k) → Option (β k)} :
(t.alter k f).get! k' = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).get! else t.get! k'
theorem Std.DTreeMap.getD_alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} :
(t.alter k f).getD k' fallback = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
theorem Std.DTreeMap.getKey?_alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.getKey!_alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.getKeyD_alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' fallback : α} {f : Option (β k) → Option (β k)} :
@[simp]
theorem Std.DTreeMap.getKeyD_alter_self {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : Option (β k) → Option (β k)} :
@[simp]
theorem Std.DTreeMap.get?_modify {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : β k → β k} :
(t.modify k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
@[simp]
theorem Std.DTreeMap.get?_modify_self {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β k → β k} :
theorem Std.DTreeMap.get!_modify {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
(t.modify k f).get! k' = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
@[simp]
theorem Std.DTreeMap.get!_modify_self {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} [Inhabited (β k)] {f : β k → β k} :
theorem Std.DTreeMap.getD_modify {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : β k → β k} :
(t.modify k f).getD k' fallback = if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
else t.getD k' fallback
@[simp]
theorem Std.DTreeMap.getD_modify_self {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {fallback : β k} {f : β k → β k} :
theorem Std.DTreeMap.getKeyD_modify {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' fallback : α} {f : β k → β k} :
@[simp]
theorem Std.DTreeMap.min?_keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [Min α] [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
@[simp]
theorem Std.DTreeMap.head?_keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [Min α] [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
theorem Std.DTreeMap.minKey?_alter_eq_self {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.maxKey?_alter_eq_self {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} :
theorem Std.DTreeMap.Equiv.insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (v : β k) :
(t₁.insertIfNew k v).Equiv (t₂.insertIfNew k v)
theorem Std.DTreeMap.Equiv.filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) (f : (a : α) → β a → Bool) :
(DTreeMap.filter f t₁).Equiv (DTreeMap.filter f t₂)
theorem Std.DTreeMap.Equiv.map {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) (f : (a : α) → β a → γ a) :
(DTreeMap.map f t₁).Equiv (DTreeMap.map f t₂)
theorem Std.DTreeMap.Equiv.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) (f : (a : α) → β a → Option (γ a)) :
(DTreeMap.filterMap f t₁).Equiv (DTreeMap.filterMap f t₂)
theorem Std.DTreeMap.Equiv.insertMany_list {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (l : List ((a : α) × β a)) :
(t₁.insertMany l).Equiv (t₂.insertMany l)
theorem Std.DTreeMap.Equiv.mergeWith {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (f : (a : α) → β a → β a → β a) (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) :
(DTreeMap.mergeWith f t₁ t₃).Equiv (DTreeMap.mergeWith f t₂ t₄)
theorem Std.DTreeMap.Equiv.constAlter {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (f : Option β → Option β) :
(Const.alter t₁ k f).Equiv (Const.alter t₂ k f)
theorem Std.DTreeMap.Equiv.constModify {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (f : β → β) :
(Const.modify t₁ k f).Equiv (Const.modify t₂ k f)
theorem Std.DTreeMap.Equiv.constInsertMany_list {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (l : List (α × β)) :
(Const.insertMany t₁ l).Equiv (Const.insertMany t₂ l)
theorem Std.DTreeMap.Equiv.constInsertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} (h : t₁.Equiv t₂) (l : List α) :
(Const.insertManyIfNewUnit t₁ l).Equiv (Const.insertManyIfNewUnit t₂ l)
theorem Std.DTreeMap.Equiv.constMergeWith {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ t₃ t₄ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (f : α → β → β → β) (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) :
(Const.mergeWith f t₁ t₃).Equiv (Const.mergeWith f t₂ t₄)
theorem Std.DTreeMap.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (hk : ∀ (k : α) (hk : k ∈ t₁) (hk' : k ∈ t₂), t₁.getKey k hk = t₂.getKey k hk') (hv : ∀ (k : α), Const.get? t₁ k = Const.get? t₂ k) :
t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_forall_constGet?_eq {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : ∀ (k : α), Const.get? t₁ k = Const.get? t₂ k) :
t₁.Equiv t₂
@[instance_reducible]
def Std.DTreeMap.isSetoid (α : Type u) (β : α → Type v) (cmp : α → α → Ordering := by exact compare) :
Implementation detail of the tree map
Equations
- Std.DTreeMap.isSetoid α β cmp = { r := Std.DTreeMap.Equiv, iseqv := ⋯ }
Instances For
theorem Std.DTreeMap.insertMany_list_equiv_foldl {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ : DTreeMap α β cmp} {l : List ((a : α) × β a)} :
(t₁.insertMany l).Equiv (List.foldl (fun (acc : DTreeMap α β cmp) (p : (a : α) × β a) => acc.insert p.fst p.snd) t₁ l)
theorem Std.DTreeMap.insertManyIfNew_list_equiv_foldl {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ : DTreeMap α β cmp} {l : List ((a : α) × β a)} :
(t₁.insertManyIfNew l).Equiv
(List.foldl (fun (acc : DTreeMap α β cmp) (p : (a : α) × β a) => acc.insertIfNew p.fst p.snd) t₁ l)
theorem Std.DTreeMap.Equiv.of_constToList_perm {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} :
(Const.toList t₁).Perm (Const.toList t₂) → t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_constToArray_perm {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} :
(Const.toArray t₁).Perm (Const.toArray t₂) → t₁.Equiv t₂
theorem Std.DTreeMap.Const.insertMany_list_equiv_foldl {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ : DTreeMap α (fun (x : α) => β) cmp} {l : List (α × β)} :
(insertMany t₁ l).Equiv
(List.foldl (fun (acc : DTreeMap α (fun (x : α) => β) cmp) (p : α × β) => acc.insert p.fst p.snd) t₁ l)
theorem Std.DTreeMap.Const.insertManyIfNewUnit_list_equiv_foldl {α : Type u} {cmp : α → α → Ordering} {t₁ : DTreeMap α (fun (x : α) => Unit) cmp} {l : List α} :
(insertManyIfNewUnit t₁ l).Equiv
(List.foldl (fun (acc : DTreeMap α (fun (x : α) => Unit) cmp) (a : α) => acc.insertIfNew a ()) t₁ l)
theorem Std.DTreeMap.Const.unitOfList_equiv_foldl {α : Type u} {cmp : α → α → Ordering} {l : List α} :
(unitOfList l cmp).Equiv
(List.foldl (fun (acc : DTreeMap α (fun (x : α) => Unit) cmp) (a : α) => acc.insertIfNew a ()) ∅ l)
theorem Std.DTreeMap.isEmpty_filterMap_eq_false_iff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} :
theorem Std.DTreeMap.contains_filterMap {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} :
@[simp]
theorem Std.DTreeMap.getKey?_filterMap {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} :
theorem Std.DTreeMap.getKey!_filterMap {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α} :
theorem Std.DTreeMap.getKeyD_filterMap {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k fallback : α} :
@[simp]
theorem Std.DTreeMap.Const.get?_filterMap' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} :
Simpler variant of get?_filterMap when LawfulEqCmp is available.
theorem Std.DTreeMap.Const.get_filterMap' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {h : k ∈ filterMap f t} :
Simpler variant of get_filterMap when LawfulEqCmp is available.
theorem Std.DTreeMap.Const.get!_filterMap' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited γ] {f : α → β → Option γ} {k : α} :
Simpler variant of get!_filterMap when LawfulEqCmp is available.
theorem Std.DTreeMap.Const.getD_filterMap' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ} :
Simpler variant of getD_filterMap when LawfulEqCmp is available.
theorem Std.DTreeMap.contains_filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} :
@[simp]
theorem Std.DTreeMap.get?_filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} :
theorem Std.DTreeMap.getD_filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α} {fallback : β k} :
theorem Std.DTreeMap.keys_filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} :
theorem Std.DTreeMap.getKey!_filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {f : (a : α) → β a → Bool} {k : α} :
theorem Std.DTreeMap.getKeyD_filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k fallback : α} :
@[simp]
theorem Std.DTreeMap.Const.get?_filter' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Bool} {k : α} :
Simpler variant of get?_filter when LawfulEqCmp is available.
theorem Std.DTreeMap.Const.get!_filter' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited β] {f : α → β → Bool} {k : α} :
Simpler variant of get!_filter when LawfulEqCmp is available.
theorem Std.DTreeMap.Const.getD_filter' {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → Bool} {k : α} {fallback : β} :
Simpler variant of getD_filter when LawfulEqCmp is available.
@[simp]
theorem Std.DTreeMap.get?_map {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} :
theorem Std.DTreeMap.getD_map {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} {γ : α → Type w} [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k} :
@[simp]
theorem Std.DTreeMap.Const.get?_map {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → γ} {k : α} :
theorem Std.DTreeMap.Const.getD_map {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {f : α → β → γ} {k : α} {fallback : γ} :