Documentation

Std.Data.DTreeMap.Internal.Model

Model implementations of tree map functions #

General infrastructure #

def Std.DTreeMap.Internal.Impl.contains' {α : Type u} {β : αType v} [Ord α] (k : αOrdering) (l : Impl α β) :

Internal implementation detail of the tree map

Equations
theorem Std.DTreeMap.Internal.Impl.contains'_compare {α : Type u} {β : αType v} [Ord α] {k : α} {l : Impl α β} :
def Std.DTreeMap.Internal.Impl.applyPartition {α : Type u} {β : αType v} {δ : Type w} [Ord α] (k : αOrdering) (l : Impl α β) (f : List ((a : α) × β a)(c : Cell α β k) → (contains' k l = truec.contains = true)List ((a : α) × β a)δ) :
δ

General tree-traversal function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.applyPartition.go {α : Type u} {β : αType v} {δ : Type w} [Ord α] (k : αOrdering) (l : Impl α β) (f : List ((a : α) × β a)(c : Cell α β k) → (contains' k l = truec.contains = true)List ((a : α) × β a)δ) (ll : List ((a : α) × β a)) (m : Impl α β) (hm : contains' k l = truecontains' k m = true) (rr : List ((a : α) × β a)) :
δ
Equations
def Std.DTreeMap.Internal.Impl.applyCell {α : Type u} {β : αType v} {δ : Type w} [Ord α] (k : α) (l : Impl α β) (f : (c : Cell α β (compare k)) → (contains' (compare k) l = truec.contains = true)δ) :
δ

Internal implementation detail of the tree map

Equations
theorem Std.DTreeMap.Internal.Impl.applyCell_eq_applyPartition {α : Type u} {β : αType v} {δ : Type w} [Ord α] (k : α) (l : Impl α β) (f : (c : Cell α β (compare k)) → (contains' (compare k) l = truec.contains = true)δ) :
applyCell k l f = applyPartition (compare k) l fun (x : List ((a : α) × β a)) (c : Cell α β (compare k)) (hc : contains' (compare k) l = truec.contains = true) (x : List ((a : α) × β a)) => f c hc

Internal implementation detail of the tree map

inductive Std.DTreeMap.Internal.Impl.ExplorationStep (α : Type u) (β : αType v) [Ord α] (k : αOrdering) :
Type (max u v)

Data structure used by the general tree-traversal function explore. Internal implementation detail of the tree map

  • lt {α : Type u} {β : αType v} [Ord α] {k : αOrdering} (a : α) : k a = Ordering.ltβ aList ((a : α) × β a)ExplorationStep α β k

    Needle was less than key at this node: return key-value pair and unexplored right subtree, recursion will continue in left subtree.

  • eq {α : Type u} {β : αType v} [Ord α] {k : αOrdering} : List ((a : α) × β a)Cell α β kList ((a : α) × β a)ExplorationStep α β k

    Needle was equal to key at this node: return key-value pair and both unexplored subtrees, recursion will terminate.

  • gt {α : Type u} {β : αType v} [Ord α] {k : αOrdering} : List ((a : α) × β a)(a : α) → k a = Ordering.gtβ aExplorationStep α β k

    Needle was larger than key at this node: return key-value pair and unexplored left subtree, recursion will containue in right subtree.

def Std.DTreeMap.Internal.Impl.explore {α : Type u} {β : αType v} {γ : Type w} [Ord α] (k : αOrdering) (init : γ) (inner : γExplorationStep α β kγ) (l : Impl α β) :
γ

General tree-traversal function. Internal implementation detail of the tree map

Equations
theorem Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.ltα} {eq : o = Ordering.eqα} {gt : o = Ordering.gtα} {lt' : o' = Ordering.ltα} {eq' : o' = Ordering.eqα} {gt' : o' = Ordering.gtα} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt = gt' h) :
(match h : o with | Ordering.lt => lt h | Ordering.eq => eq h | Ordering.gt => gt h) = match h : o' with | Ordering.lt => lt' h | Ordering.eq => eq' h | Ordering.gt => gt' h
theorem Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.ltα} {eq : o = Ordering.eqα} {gt : o = Ordering.gtα} {lt' : o' = Ordering.ltα} {eq' : o' = Ordering.eqα} {gt' : o' = Ordering.gtα} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt = gt' h) :
(match h : o with | Ordering.lt => lt h | Ordering.eq => eq h | Ordering.gt => gt h) = match h : o' with | Ordering.lt => lt' h | Ordering.eq => eq' h | Ordering.gt => gt' h
theorem Std.DTreeMap.Internal.Impl.getEntryLE.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.ltα} {eq : o = Ordering.eqα} {gt : o = Ordering.gtα} {lt' : o' = Ordering.ltα} {eq' : o' = Ordering.eqα} {gt' : o' = Ordering.gtα} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt = gt' h) :
(match hkky : o with | Ordering.gt => gt hkky | Ordering.eq => eq hkky | Ordering.lt => lt hkky) = match hkky : o' with | Ordering.gt => gt' hkky | Ordering.eq => eq' hkky | Ordering.lt => lt' hkky
theorem Std.DTreeMap.Internal.Impl.get?.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.ltα} {eq : o = Ordering.eqα} {gt : o = Ordering.gtα} {lt' : o' = Ordering.ltα} {eq' : o' = Ordering.eqα} {gt' : o' = Ordering.gtα} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt = gt' h) :
(match h : o with | Ordering.lt => lt h | Ordering.gt => gt h | Ordering.eq => eq h) = match h : o' with | Ordering.lt => lt' h | Ordering.gt => gt' h | Ordering.eq => eq' h
theorem Std.DTreeMap.Internal.Impl.tree_split_ind_no_gen {α : Type u} {β : αType v} [Ord α] (k : αOrdering) {motive : Impl α βProp} (leaf : motive leaf) (lt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.ltmotive lmotive (inner n ky y l r)) (eq : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.eqmotive lmotive rmotive (inner n ky y l r)) (gt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.gtmotive rmotive (inner n ky y l r)) (t : Impl α β) :
motive t

Induction principle on Impl with an additional case split on k ky for Impl.inner _ ky _ _ _ without generalization.

theorem Std.DTreeMap.Internal.Impl.tree_split_ind {α : Type u} {β : αType v} {γ : Sort w} [Ord α] (k : αOrdering) {motive : Impl α βγProp} (leaf : ∀ (x : γ), motive leaf x) (lt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.lt(∀ (x : γ), motive l x)∀ (x : γ), motive (inner n ky y l r) x) (eq : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.eq(∀ (x : γ), motive l x)(∀ (x : γ), motive r x)∀ (x : γ), motive (inner n ky y l r) x) (gt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.gt(∀ (x : γ), motive r x)∀ (x : γ), motive (inner n ky y l r) x) (t : Impl α β) (x : γ) :
motive t x

Induction principle on Impl with an additional case split on k ky for Impl.inner _ ky _ _ _ and a generalization built in for convenience.

theorem Std.DTreeMap.Internal.Impl.applyPartition_go_step {α : Type u} {β : αType v} {δ : Type w} [Ord α] {k : αOrdering} {init : δ} (l₁ l₂ : List ((a : α) × β a)) (l l' : Impl α β) (h : contains' k l' = truecontains' k l = true) (f : δExplorationStep α β kδ) :
applyPartition.go k l' (fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = truec.contains = true) (r' : List ((a : α) × β a)) => f init (ExplorationStep.eq l'_1 c r')) l₁ l h l₂ = applyPartition.go k l' (fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = truec.contains = true) (r' : List ((a : α) × β a)) => f init (ExplorationStep.eq (l₁ ++ l'_1) c (r' ++ l₂))) [] l h []
theorem Std.DTreeMap.Internal.Impl.explore_eq_applyPartition {α : Type u} {β : αType v} {δ : Type w} [Ord α] {k : αOrdering} (init : δ) (l : Impl α β) (f : δExplorationStep α β kδ) (hfr : ∀ {k_1 : α} {hk : k k_1 = Ordering.lt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Cell α β k} {rr r : List ((a : α) × β a)} {init : δ}, f (f init (ExplorationStep.lt k_1 hk v r)) (ExplorationStep.eq ll c rr) = f init (ExplorationStep.eq ll c (rr ++ k_1, v :: r))) (hfl : ∀ {k_1 : α} {hk : k k_1 = Ordering.gt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Cell α β k} {rr l : List ((a : α) × β a)} {init : δ}, f (f init (ExplorationStep.gt l k_1 hk v)) (ExplorationStep.eq ll c rr) = f init (ExplorationStep.eq (l ++ k_1, v :: ll) c rr)) :
explore k init f l = applyPartition k l fun (l_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l = truec.contains = true) (r : List ((a : α) × β a)) => f init (ExplorationStep.eq l_1 c r)
noncomputable def Std.DTreeMap.Internal.Impl.updateCell {α : Type u} {β : αType v} [Ord α] (k : α) (f : Cell α β (compare k)Cell α β (compare k)) (l : Impl α β) (hl : l.Balanced) :
SizedBalancedTree α β (l.size - 1) (l.size + 1)

General "update the mapping for a given key" function. Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.

Model functions #

def Std.DTreeMap.Internal.Impl.containsₘ {α : Type u} {β : αType v} [Ord α] (l : Impl α β) (k : α) :

Model implementation of the contains function. Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.get?ₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) :
Option (β k)

Model implementation of the get? function. Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.getₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) (h : (l.get?ₘ k).isSome = true) :
β k

Model implementation of the get function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.get!ₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) [Inhabited (β k)] :
β k

Model implementation of the get! function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.getDₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) (fallback : β k) :
β k

Model implementation of the getD function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.getKey?ₘ {α : Type u} {β : αType v} [Ord α] (l : Impl α β) (k : α) :

Model implementation of the getKey? function. Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.getKeyₘ {α : Type u} {β : αType v} [Ord α] (l : Impl α β) (k : α) (h : (l.getKey?ₘ k).isSome = true) :
α

Model implementation of the getKey function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.getKey!ₘ {α : Type u} {β : αType v} [Ord α] (l : Impl α β) (k : α) [Inhabited α] :
α

Model implementation of the getKey! function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.getKeyDₘ {α : Type u} {β : αType v} [Ord α] (k : α) (l : Impl α β) (fallback : α) :
α

Model implementation of the getKeyD function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.minEntry?ₘ' {α : Type u} {β : αType v} [Ord α] (l : Impl α β) :
Option ((a : α) × β a)

Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.minEntry?ₘ {α : Type u} {β : αType v} [Ord α] (l : Impl α β) :
Option ((a : α) × β a)

Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.reverse {α : Type u} {β : αType v} :
Impl α βImpl α β

Internal implementation detail of the tree map

Equations
noncomputable def Std.DTreeMap.Internal.Impl.insertₘ {α : Type u} {β : αType v} [Ord α] (k : α) (v : β k) (l : Impl α β) (h : l.Balanced) :
Impl α β

Model implementation of the insert function. Internal implementation detail of the tree map

Equations
noncomputable def Std.DTreeMap.Internal.Impl.eraseₘ {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) (h : t.Balanced) :
Impl α β

Model implementation of the erase function. Internal implementation detail of the tree map

Equations
noncomputable def Std.DTreeMap.Internal.Impl.insertIfNewₘ {α : Type u} {β : αType v} [Ord α] (k : α) (v : β k) (l : Impl α β) (h : l.Balanced) :
Impl α β

Model implementation of the insertIfNew function. Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Std.DTreeMap.Internal.Impl.alterₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (f : Option (β k)Option (β k)) (t : Impl α β) (h : t.Balanced) :
Impl α β

Model implementation of the alter function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.Const.get?ₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) :

Model implementation of the get? function. Internal implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.Const.getₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) (h : (get?ₘ l k).isSome = true) :
β

Model implementation of the get function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.Const.get!ₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) [Inhabited β] :
β

Model implementation of the get! function. Internal implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.Const.getDₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) (fallback : β) :
β

Model implementation of the getD function. Internal implementation detail of the tree map

Equations
noncomputable def Std.DTreeMap.Internal.Impl.Const.alterₘ {α : Type u} {β : Type v} [Ord α] [OrientedOrd α] (k : α) (f : Option βOption β) (t : Impl α fun (x : α) => β) (h : t.Balanced) :
Impl α fun (x : α) => β

Model implementation of the alter function. Internal implementation detail of the tree map

Equations

Helper theorems for reasoning with key-value pairs #

theorem Std.DTreeMap.Internal.Impl.balanceL!_pair_congr {α : Type u} {β : αType v} {k : α} {v : β k} {k' : α} {v' : β k'} (h : k, v = k', v') {l l' r r' : Impl α β} (hl : l = l') (hr : r = r') :
balanceL! k v l r = balanceL! k' v' l' r'
theorem Std.DTreeMap.Internal.Impl.balanceR!_pair_congr {α : Type u} {β : αType v} {k : α} {v : β k} {k' : α} {v' : β k'} (h : k, v = k', v') {l l' r r' : Impl α β} (hl : l = l') (hr : r = r') :
balanceR! k v l r = balanceR! k' v' l' r'

Equivalence of function to model functions #

theorem Std.DTreeMap.Internal.Impl.contains_eq_containsₘ {α : Type u} {β : αType v} [Ord α] (k : α) (l : Impl α β) :
theorem Std.DTreeMap.Internal.Impl.get?_eq_get?ₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) :
l.get? k = l.get?ₘ k
theorem Std.DTreeMap.Internal.Impl.get_eq_get? {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) {h : k l} :
some (l.get k h) = l.get? k
theorem Std.DTreeMap.Internal.Impl.get_eq_getₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) {h : k l} (h' : (l.get?ₘ k).isSome = true) :
l.get k h = l.getₘ k h'
theorem Std.DTreeMap.Internal.Impl.get!_eq_get!ₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) [Inhabited (β k)] (l : Impl α β) :
l.get! k = l.get!ₘ k
theorem Std.DTreeMap.Internal.Impl.getD_eq_getDₘ {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) (fallback : β k) :
l.getD k fallback = getDₘ k l fallback
theorem Std.DTreeMap.Internal.Impl.getKey?_eq_getKey?ₘ {α : Type u} {β : αType v} [Ord α] (k : α) (l : Impl α β) :
theorem Std.DTreeMap.Internal.Impl.getKey_eq_getKey? {α : Type u} {β : αType v} [Ord α] (k : α) (l : Impl α β) {h : contains k l = true} :
some (l.getKey k h) = l.getKey? k
theorem Std.DTreeMap.Internal.Impl.getKey_eq_getKeyₘ {α : Type u} {β : αType v} [Ord α] (k : α) (l : Impl α β) {h : contains k l = true} (h' : (l.getKey?ₘ k).isSome = true) :
l.getKey k h = l.getKeyₘ k h'
theorem Std.DTreeMap.Internal.Impl.getKey!_eq_getKey!ₘ {α : Type u} {β : αType v} [Ord α] (k : α) [Inhabited α] (l : Impl α β) :
theorem Std.DTreeMap.Internal.Impl.getKeyD_eq_getKeyDₘ {α : Type u} {β : αType v} [Ord α] (k : α) (l : Impl α β) (fallback : α) :
l.getKeyD k fallback = getKeyDₘ k l fallback
theorem Std.DTreeMap.Internal.Impl.minEntry!_eq_get!_minEntry? {α : Type u} {β : αType v} [Inhabited ((a : α) × β a)] {l : Impl α β} :
theorem Std.DTreeMap.Internal.Impl.minEntryD_eq_getD_minEntry? {α : Type u} {β : αType v} {l : Impl α β} {fallback : (a : α) × β a} :
l.minEntryD fallback = l.minEntry?.getD fallback
theorem Std.DTreeMap.Internal.Impl.some_minEntry_eq_minEntry? {α : Type u} {β : αType v} {l : Impl α β} {he : l.isEmpty = false} :
theorem Std.DTreeMap.Internal.Impl.minEntry_eq_get_minEntry? {α : Type u} {β : αType v} {l : Impl α β} {he : l.isEmpty = false} :
l.minEntry he = l.minEntry?.get
theorem Std.DTreeMap.Internal.Impl.maxEntry!_eq_get!_maxEntry? {α : Type u} {β : αType v} [Inhabited ((a : α) × β a)] {l : Impl α β} :
theorem Std.DTreeMap.Internal.Impl.maxEntryD_eq_getD_maxEntry? {α : Type u} {β : αType v} {l : Impl α β} {fallback : (a : α) × β a} :
l.maxEntryD fallback = l.maxEntry?.getD fallback
theorem Std.DTreeMap.Internal.Impl.some_maxEntry_eq_maxEntry? {α : Type u} {β : αType v} {l : Impl α β} {he : l.isEmpty = false} :
theorem Std.DTreeMap.Internal.Impl.minKey_eq_minEntry_fst {α : Type u} {β : αType v} {l : Impl α β} {he : l.isEmpty = false} :
l.minKey he = (l.minEntry he).fst
theorem Std.DTreeMap.Internal.Impl.minKeyD_eq_getD_minKey? {α : Type u} {β : αType v} {l : Impl α β} {fallback : α} :
l.minKeyD fallback = l.minKey?.getD fallback
theorem Std.DTreeMap.Internal.Impl.some_maxKey_eq_maxKey? {α : Type u} {β : αType v} {l : Impl α β} {he : l.isEmpty = false} :
some (l.maxKey he) = l.maxKey?
theorem Std.DTreeMap.Internal.Impl.maxKey_eq_get_maxKey? {α : Type u} {β : αType v} {l : Impl α β} {he : l.isEmpty = false} :
l.maxKey he = l.maxKey?.get
theorem Std.DTreeMap.Internal.Impl.maxKeyD_eq_getD_maxKey? {α : Type u} {β : αType v} {l : Impl α β} {fallback : α} :
l.maxKeyD fallback = l.maxKey?.getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.minEntry?_eq_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} :
minEntry? l = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l.minEntry?
theorem Std.DTreeMap.Internal.Impl.Const.minEntry!_eq_get!_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.minEntryD_eq_getD_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {fallback : α × β} :
minEntryD l fallback = (minEntry? l).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.some_minEntry_eq_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {he : l.isEmpty = false} :
theorem Std.DTreeMap.Internal.Impl.Const.maxEntry?_eq_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} :
maxEntry? l = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l.maxEntry?
theorem Std.DTreeMap.Internal.Impl.Const.maxEntry!_eq_get!_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.maxEntryD_eq_getD_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {fallback : α × β} :
maxEntryD l fallback = (maxEntry? l).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.some_maxEntry_eq_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {he : l.isEmpty = false} :
theorem Std.DTreeMap.Internal.Impl.balanceL_eq_balance {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond l.size r.size} :
balanceL k v l r hlb hrb hlr = balance k v l r hlb hrb
theorem Std.DTreeMap.Internal.Impl.balanceR_eq_balance {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond r.size l.size} :
balanceR k v l r hlb hrb hlr = balance k v l r hlb hrb
theorem Std.DTreeMap.Internal.Impl.balanceLErase_eq_balance {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size} :
balanceLErase k v l r hlb hrb hlr = balance k v l r hlb hrb
theorem Std.DTreeMap.Internal.Impl.balanceRErase_eq_balance {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond r.size l.size} :
balanceRErase k v l r hlb hrb hlr = balance k v l r hlb hrb
theorem Std.DTreeMap.Internal.Impl.balanceL_eq_balanceL! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond l.size r.size} :
balanceL k v l r hlb hrb hlr = balanceL! k v l r
theorem Std.DTreeMap.Internal.Impl.balanceR_eq_balanceR! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond r.size l.size} :
balanceR k v l r hlb hrb hlr = balanceR! k v l r
theorem Std.DTreeMap.Internal.Impl.minView_k_eq_minView! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
(minView k v l r hl hr hlr).k = (minView! k v l r).k
theorem Std.DTreeMap.Internal.Impl.minView_kv_eq_minView! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
(minView k v l r hl hr hlr).k, (minView k v l r hl hr hlr).v = (minView! k v l r).k, (minView! k v l r).v
theorem Std.DTreeMap.Internal.Impl.minView_tree_impl_eq_minView! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
(minView k v l r hl hr hlr).tree.impl = (minView! k v l r).tree
theorem Std.DTreeMap.Internal.Impl.maxView_k_eq_maxView! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
(maxView k v l r hl hr hlr).k = (maxView! k v l r).k
theorem Std.DTreeMap.Internal.Impl.maxView_kv_eq_maxView! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
(maxView k v l r hl hr hlr).k, (maxView k v l r hl hr hlr).v = (maxView! k v l r).k, (maxView! k v l r).v
theorem Std.DTreeMap.Internal.Impl.maxView_tree_impl_eq_maxView! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
(maxView k v l r hl hr hlr).tree.impl = (maxView! k v l r).tree
theorem Std.DTreeMap.Internal.Impl.glue_eq_glue! {α : Type u} {β : αType v} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} :
l.glue r hl hr hlr = l.glue! r
theorem Std.DTreeMap.Internal.Impl.insert_eq_insert! {α : Type u} {β : αType v} [Ord α] {k : α} {v : β k} {l : Impl α β} {h : l.Balanced} :
(insert k v l h).impl = insert! k v l
theorem Std.DTreeMap.Internal.Impl.insert_eq_insertₘ {α : Type u} {β : αType v} [Ord α] {k : α} {v : β k} {l : Impl α β} {h : l.Balanced} :
(insert k v l h).impl = insertₘ k v l h
theorem Std.DTreeMap.Internal.Impl.insert!_eq_insertₘ {α : Type u} {β : αType v} [Ord α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) :
insert! k v l = insertₘ k v l h
theorem Std.DTreeMap.Internal.Impl.erase_eq_erase! {α : Type u} {β : αType v} [Ord α] {k : α} {t : Impl α β} {h : t.Balanced} :
(erase k t h).impl = erase! k t
theorem Std.DTreeMap.Internal.Impl.erase_eq_eraseₘ {α : Type u} {β : αType v} [Ord α] {k : α} {t : Impl α β} {h : t.Balanced} :
(erase k t h).impl = eraseₘ k t h
theorem Std.DTreeMap.Internal.Impl.erase!_eq_eraseₘ {α : Type u} {β : αType v} [Ord α] {k : α} {t : Impl α β} (h : t.Balanced) :
erase! k t = eraseₘ k t h
theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_fst_eq_containsThenInsert_fst {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_containsThenInsert_snd {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
theorem Std.DTreeMap.Internal.Impl.containsThenInsert_snd_eq_insertₘ {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
(containsThenInsert a b t htb).snd.impl = insertₘ a b t htb
theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_insertₘ {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
theorem Std.DTreeMap.Internal.Impl.insertIfNew_eq_insertIfNew! {α : Type u} {β : αType v} [Ord α] {k : α} {v : β k} {l : Impl α β} {h : l.Balanced} :
(insertIfNew k v l h).impl = insertIfNew! k v l
theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst_eq_containsₘ {α : Type u} {β : αType v} [Ord α] [TransOrd α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_snd_eq_insertIfNew {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsₘ {α : Type u} {β : αType v} [Ord α] [TransOrd α] (t : Impl α β) (a : α) (b : β a) :
theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_insertIfNew! {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (a : α) (b : β a) :
@[irreducible]
theorem Std.DTreeMap.Internal.Impl.insertMin_eq_insertMin! {α : Type u} {β : αType v} [Ord α] {a : α} {b : β a} {t : Impl α β} (htb : t.Balanced) :
(insertMin a b t htb).impl = insertMin! a b t
@[irreducible]
theorem Std.DTreeMap.Internal.Impl.insertMax_eq_insertMax! {α : Type u} {β : αType v} [Ord α] {a : α} {b : β a} {t : Impl α β} (htb : t.Balanced) :
(insertMax a b t htb).impl = insertMax! a b t
theorem Std.DTreeMap.Internal.Impl.link2_eq_link2! {α : Type u} {β : αType v} [Ord α] {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) :
(l.link2 r hlb hrb).impl = l.link2! r
theorem Std.DTreeMap.Internal.Impl.Const.get?_eq_get?ₘ {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) :
get? l k = get?ₘ l k
theorem Std.DTreeMap.Internal.Impl.Const.get_eq_get? {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) {h : contains k l = true} :
some (get l k h) = get? l k
theorem Std.DTreeMap.Internal.Impl.Const.get_eq_getₘ {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) {h : contains k l = true} (h' : (get?ₘ l k).isSome = true) :
get l k h = getₘ l k h'
theorem Std.DTreeMap.Internal.Impl.Const.get!_eq_get!ₘ {α : Type u} {β : Type v} [Ord α] (k : α) [Inhabited β] (l : Impl α fun (x : α) => β) :
get! l k = get!ₘ l k
theorem Std.DTreeMap.Internal.Impl.Const.getD_eq_getDₘ {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) (fallback : β) :
getD l k fallback = getDₘ l k fallback
theorem Std.DTreeMap.Internal.Impl.entryAtIdx?_eq_some_entryAtIdx {α : Type u} {β : αType v} {t : Impl α β} (htb : t.Balanced) {i : Nat} (h : i < t.size) :
t.entryAtIdx? i = some (t.entryAtIdx htb i h)
theorem Std.DTreeMap.Internal.Impl.entryAtIdx!_eq_get!_entryAtIdx? {α : Type u} {β : αType v} {t : Impl α β} {i : Nat} [Inhabited ((a : α) × β a)] :
theorem Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD_entryAtIdx? {α : Type u} {β : αType v} {t : Impl α β} {i : Nat} {fallback : (a : α) × β a} :
t.entryAtIdxD i fallback = (t.entryAtIdx? i).getD fallback
theorem Std.DTreeMap.Internal.Impl.keyAtIdx?_eq_entryAtIdx? {α : Type u} {β : αType v} {t : Impl α β} {i : Nat} :
t.keyAtIdx? i = Option.map (fun (x : (a : α) × β a) => x.fst) (t.entryAtIdx? i)
theorem Std.DTreeMap.Internal.Impl.keyAtIdx_eq_entryAtIdx_fst {α : Type u} {β : αType v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {h : i < t.size} :
t.keyAtIdx htb i h = (t.entryAtIdx htb i h).fst
theorem Std.DTreeMap.Internal.Impl.keyAtIdx!_eq_get!_keyAtIdx? {α : Type u} {β : αType v} [Inhabited α] {t : Impl α β} {i : Nat} :
theorem Std.DTreeMap.Internal.Impl.keyAtIdxD_eq_getD_keyAtIdx? {α : Type u} {β : αType v} {t : Impl α β} {i : Nat} {fallback : α} :
t.keyAtIdxD i fallback = (t.keyAtIdx? i).getD fallback
def Std.DTreeMap.Internal.Impl.getEntryGE?ₘ {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
Option ((a : α) × β a)

Implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.getEntryGE?ₘ' {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
Option ((a : α) × β a)

Implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
theorem Std.DTreeMap.Internal.Impl.getEntryGE?_eq_getEntryGE?ₘ' {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
theorem Std.DTreeMap.Internal.Impl.getEntryGE?_eq_getEntryGE?ₘ {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
def Std.DTreeMap.Internal.Impl.getEntryGT?ₘ {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
Option ((a : α) × β a)

Implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DTreeMap.Internal.Impl.getEntryGT?ₘ' {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
Option ((a : α) × β a)

Implementation detail of the tree map

Equations
  • One or more equations did not get rendered due to their size.
theorem Std.DTreeMap.Internal.Impl.getEntryGT?_eq_getEntryGT?ₘ' {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
theorem Std.DTreeMap.Internal.Impl.getEntryGT?_eq_getEntryGT?ₘ {α : Type u} {β : αType v} [Ord α] (k : α) (t : Impl α β) :
theorem Std.DTreeMap.Internal.Impl.getEntryLT?_eq_getEntryGT?_reverse {α : Type u} {β : αType v} [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} :
theorem Std.DTreeMap.Internal.Impl.getEntryLE?_eq_getEntryGE?_reverse {α : Type u} {β : αType v} [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} :
theorem Std.DTreeMap.Internal.Impl.getEntryGE!_eq_get!_getEntryGE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] :
theorem Std.DTreeMap.Internal.Impl.getEntryGT!_eq_get!_getEntryGT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] :
theorem Std.DTreeMap.Internal.Impl.getEntryLE!_eq_get!_getEntryLE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] :
theorem Std.DTreeMap.Internal.Impl.getEntryLT!_eq_get!_getEntryLT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] :
theorem Std.DTreeMap.Internal.Impl.getEntryGED_eq_getD_getEntryGE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} :
getEntryGED k t fallback = (getEntryGE? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getEntryGTD_eq_getD_getEntryGT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} :
getEntryGTD k t fallback = (getEntryGT? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getEntryLED_eq_getD_getEntryLE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} :
getEntryLED k t fallback = (getEntryLE? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getEntryLTD_eq_getD_getEntryLT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} :
getEntryLTD k t fallback = (getEntryLT? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getEntryGE?.eq_go {α : Type u} {β : αType v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) :
(getEntryGE? k t).or x = go k x t
theorem Std.DTreeMap.Internal.Impl.getEntryGT?.eq_go {α : Type u} {β : αType v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) :
(getEntryGT? k t).or x = go k x t
theorem Std.DTreeMap.Internal.Impl.getEntryLE?.eq_go {α : Type u} {β : αType v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) :
(getEntryLE? k t).or x = go k x t
theorem Std.DTreeMap.Internal.Impl.getEntryLT?.eq_go {α : Type u} {β : αType v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) :
(getEntryLT? k t).or x = go k x t
theorem Std.DTreeMap.Internal.Impl.some_getEntryGE_eq_getEntryGE? {α : Type u} {β : αType v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : (a : α), a t (compare a k).isGE = true} :
some (getEntryGE k t ho he) = getEntryGE? k t
theorem Std.DTreeMap.Internal.Impl.some_getEntryGT_eq_getEntryGT? {α : Type u} {β : αType v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : (a : α), a t compare a k = Ordering.gt} :
some (getEntryGT k t ho he) = getEntryGT? k t
theorem Std.DTreeMap.Internal.Impl.some_getEntryLE_eq_getEntryLE? {α : Type u} {β : αType v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : (a : α), a t (compare a k).isLE = true} :
some (getEntryLE k t ho he) = getEntryLE? k t
theorem Std.DTreeMap.Internal.Impl.some_getEntryLT_eq_getEntryLT? {α : Type u} {β : αType v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : (a : α), a t compare a k = Ordering.lt} :
some (getEntryLT k t ho he) = getEntryLT? k t
theorem Std.DTreeMap.Internal.Impl.getKeyGE?_eq_getEntryGE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} :
getKeyGE? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryGE? k t)
theorem Std.DTreeMap.Internal.Impl.getKeyGT?_eq_getEntryGT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} :
getKeyGT? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryGT? k t)
theorem Std.DTreeMap.Internal.Impl.getKeyLE?_eq_getEntryLE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} :
getKeyLE? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryLE? k t)
theorem Std.DTreeMap.Internal.Impl.getKeyLT?_eq_getEntryLT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} :
getKeyLT? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryLT? k t)
theorem Std.DTreeMap.Internal.Impl.getKeyGE!_eq_get!_getKeyGE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] :
theorem Std.DTreeMap.Internal.Impl.getKeyGT!_eq_get!_getKeyGT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] :
theorem Std.DTreeMap.Internal.Impl.getKeyLE!_eq_get!_getKeyLE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] :
theorem Std.DTreeMap.Internal.Impl.getKeyLT!_eq_get!_getKeyLT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] :
theorem Std.DTreeMap.Internal.Impl.getKeyGED_eq_getD_getKeyGE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k fallback : α} :
getKeyGED k t fallback = (getKeyGE? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getKeyGTD_eq_getD_getKeyGT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k fallback : α} :
getKeyGTD k t fallback = (getKeyGT? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getKeyLED_eq_getD_getKeyLE? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k fallback : α} :
getKeyLED k t fallback = (getKeyLE? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getKeyLTD_eq_getD_getKeyLT? {α : Type u} {β : αType v} [Ord α] {t : Impl α β} {k fallback : α} :
getKeyLTD k t fallback = (getKeyLT? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.getKeyGE_eq_getEntryGE {α : Type u} {β : αType v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : (a : α), a t (compare a k).isGE = true} :
getKeyGE k t hto he = (getEntryGE k t hto he).fst
theorem Std.DTreeMap.Internal.Impl.getKeyGT_eq_getEntryGT {α : Type u} {β : αType v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : (a : α), a t compare a k = Ordering.gt} :
getKeyGT k t hto he = (getEntryGT k t hto he).fst
theorem Std.DTreeMap.Internal.Impl.getKeyLE_eq_getEntryLE {α : Type u} {β : αType v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : (a : α), a t (compare a k).isLE = true} :
getKeyLE k t hto he = (getEntryLE k t hto he).fst
theorem Std.DTreeMap.Internal.Impl.getKeyLT_eq_getEntryLT {α : Type u} {β : αType v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : (a : α), a t compare a k = Ordering.lt} :
getKeyLT k t hto he = (getEntryLT k t hto he).fst
theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx?_eq_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} {i : Nat} :
entryAtIdx? t i = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (t.entryAtIdx? i)
theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx_eq {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} {h : i < t.size} :
entryAtIdx t htb i h = ((t.entryAtIdx htb i h).fst, (t.entryAtIdx htb i h).snd)
theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx!_eq_get!_entryAtIdx? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} {i : Nat} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdxD_eq_getD_entryAtIdx? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} {i : Nat} {fallback : α × β} :
entryAtIdxD t i fallback = (entryAtIdx? t i).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGE?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} :
getEntryGE? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryGE? k t)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGT?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} :
getEntryGT? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryGT? k t)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLE?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} :
getEntryLE? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryLE? k t)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLT?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} :
getEntryLT? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryLT? k t)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGE!_eq_get!_getEntryGE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGT!_eq_get!_getEntryGT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLE!_eq_get!_getEntryLE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLT!_eq_get!_getEntryLT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] :
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGED_eq_getD_getEntryGE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} :
getEntryGED k t fallback = (getEntryGE? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGTD_eq_getD_getEntryGT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} :
getEntryGTD k t fallback = (getEntryGT? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLED_eq_getD_getEntryLE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} :
getEntryLED k t fallback = (getEntryLE? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLTD_eq_getD_getEntryLT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} :
getEntryLTD k t fallback = (getEntryLT? k t).getD fallback
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGE_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : (a : α), a t (compare a k).isGE = true) :
getEntryGE k t hto he = ((Impl.getEntryGE k t hto he).fst, (Impl.getEntryGE k t hto he).snd)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryGT_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : (a : α), a t compare a k = Ordering.gt) :
getEntryGT k t hto he = ((Impl.getEntryGT k t hto he).fst, (Impl.getEntryGT k t hto he).snd)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLE_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : (a : α), a t (compare a k).isLE = true) :
getEntryLE k t hto he = ((Impl.getEntryLE k t hto he).fst, (Impl.getEntryLE k t hto he).snd)
theorem Std.DTreeMap.Internal.Impl.Const.getEntryLT_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : (a : α), a t compare a k = Ordering.lt) :
getEntryLT k t hto he = ((Impl.getEntryLT k t hto he).fst, (Impl.getEntryLT k t hto he).snd)