# Documentation

Std.Data.RBMap.Lemmas

# Additional lemmas for Red-black trees #

def Std.RBNode.depth {α : Type u_1} :

O(n). depth t is the maximum number of nodes on any path to a leaf. It is an upper bound on most tree operations.

Equations
Instances For
theorem Std.RBNode.size_lt_depth {α : Type u_1} (t : ) :

depthLB c n is the best upper bound on the depth of any balanced red-black tree with root colored c and black-height n.

Instances For

depthUB c n is the best upper bound on the depth of any balanced red-black tree with root colored c and black-height n.

Instances For
theorem Std.RBNode.depthUB_le (c : Std.RBColor) (n : Nat) :
2 * n + 1
theorem Std.RBNode.Balanced.depth_le {α : Type u_1} {t : } {c : Std.RBColor} {n : Nat} :
theorem Std.RBNode.Balanced.le_size {α : Type u_1} {t : } {c : Std.RBColor} {n : Nat} :
2 ^
theorem Std.RBNode.Balanced.depth_bound {α : Type u_1} {t : } {c : Std.RBColor} {n : Nat} (h : ) :
2 * Nat.log2 ()
theorem Std.RBNode.WF.depth_bound {α : Type u_1} {cmp : ααOrdering} {t : } (h : Std.RBNode.WF cmp t) :
2 * Nat.log2 ()

A well formed tree has t.depth ∈ O(log t.size), that is, it is well balanced. This justifies the O(log n) bounds on most searching operations of RBSet.

@[simp]
theorem Std.RBNode.mem_nil {α : Type u_1} {x : α} :
¬x Std.RBNode.nil
@[simp]
theorem Std.RBNode.mem_node {α : Type u_1} {y : α} {c : Std.RBColor} {a : } {x : α} {b : } :
y Std.RBNode.node c a x b y = x y a y b
theorem Std.RBNode.All_def {α : Type u_1} {p : αProp} {t : } :
(x : α) → x tp x
theorem Std.RBNode.Any_def {α : Type u_1} {p : αProp} {t : } :
x, x t p x
theorem Std.RBNode.memP_def :
∀ {α : Type u_1} {cut : αOrdering} {t : }, Std.RBNode.MemP cut t x, x t cut x = Ordering.eq
theorem Std.RBNode.mem_def :
∀ {α : Type u_1} {cmp : ααOrdering} {x : α} {t : }, Std.RBNode.Mem cmp x t y, y t cmp x y = Ordering.eq
theorem Std.RBNode.mem_congr {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Std.TransCmp cmp] {t : } (h : cmp x y = Ordering.eq) :
theorem Std.RBNode.isOrdered_iff' {α : Type u_1} {cmp : ααOrdering} {L : } {R : } [Std.TransCmp cmp] {t : } :
Std.RBNode.isOrdered cmp t L R = true (∀ (a : α), a LStd.RBNode.All (fun x => Std.RBNode.cmpLT cmp a x) t) (∀ (a : α), a RStd.RBNode.All (fun x => Std.RBNode.cmpLT cmp x a) t) (∀ (a : α), a L∀ (b : α), b RStd.RBNode.cmpLT cmp a b)
theorem Std.RBNode.isOrdered_iff {α : Type u_1} {cmp : ααOrdering} [Std.TransCmp cmp] {t : } :
Std.RBNode.isOrdered cmp t none none = true
instance Std.RBNode.instDecidableOrdered {α : Type u_1} (cmp : ααOrdering) [Std.TransCmp cmp] (t : ) :
class Std.RBNode.IsCut {α : Sort u_1} (cmp : ααOrdering) (cut : αOrdering) :

A cut is like a homomorphism of orderings: it is a monotonic predicate with respect to cmp, but it can make things that are distinguished by cmp equal. This is sufficient for find? to locate an element on which cut returns .eq, but there may be other elements, not returned by find?, on which cut also returns .eq.

Instances
theorem Std.RBNode.IsCut.lt_trans :
∀ {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} {x y : α} [inst : Std.RBNode.IsCut cmp cut] [inst : Std.TransCmp cmp], cmp x y = Ordering.ltcut x = Ordering.ltcut y = Ordering.lt
theorem Std.RBNode.IsCut.gt_trans :
∀ {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} {x y : α} [inst : Std.RBNode.IsCut cmp cut] [inst : Std.TransCmp cmp], cmp x y = Ordering.ltcut y = Ordering.gtcut x = Ordering.gt
theorem Std.RBNode.IsCut.congr :
∀ {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} {x y : α} [inst : Std.RBNode.IsCut cmp cut] [inst : Std.TransCmp cmp], cmp x y = Ordering.eqcut x = cut y
class Std.RBNode.IsStrictCut {α : Sort u_1} (cmp : ααOrdering) (cut : αOrdering) extends :

IsStrictCut upgrades the IsCut property to ensure that at most one element of the tree can match the cut, and hence find? will return the unique such element if one exists.

Instances
instance Std.RBNode.instIsStrictCut {α : Sort u_1} (cmp : ααOrdering) (a : α) :

A "representable cut" is one generated by cmp a for some a. This is always a valid cut.

theorem Std.RBNode.find?_some_eq_eq {α : Type u_1} {x : α} {cut : αOrdering} {t : } :
x Std.RBNode.find? cut tcut x = Ordering.eq
theorem Std.RBNode.find?_some_mem {α : Type u_1} {x : α} {cut : αOrdering} {t : } :
x Std.RBNode.find? cut tx t
theorem Std.RBNode.find?_some_memP {α : Type u_1} {x : α} {cut : αOrdering} {t : } (h : x Std.RBNode.find? cut t) :
theorem Std.RBNode.Ordered.memP_iff_find? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (ht : ) :
theorem Std.RBNode.Ordered.unique {α : Type u_1} {cmp : ααOrdering} {t : } {x : α} {y : α} [Std.TransCmp cmp] (ht : ) (hx : x t) (hy : y t) (e : cmp x y = Ordering.eq) :
x = y
theorem Std.RBNode.Ordered.find?_some {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } {x : α} [Std.TransCmp cmp] [Std.RBNode.IsStrictCut cmp cut] (ht : ) :
theorem Std.RBNode.lowerBound?_le' {α : Type u_1} {lb : } {cut : αOrdering} {x : α} {t : } (H : ∀ {x : α}, x lbcut x Ordering.lt) :

The value x returned by lowerBound? is less or equal to the cut.

theorem Std.RBNode.lowerBound?_le {α : Type u_1} {cut : αOrdering} {x : α} {t : } :

The value x returned by lowerBound? is less or equal to the cut.

theorem Std.RBNode.All.lowerBound?_lb {α : Type u_1} {p : αProp} {lb : } {cut : αOrdering} {x : α} {t : } (hp : ) (H : {x : α} → x lbp x) :
Std.RBNode.lowerBound? cut t lb = some xp x
theorem Std.RBNode.All.lowerBound? {α : Type u_1} {p : αProp} {cut : αOrdering} {x : α} {t : } (hp : ) :
Std.RBNode.lowerBound? cut t none = some xp x
theorem Std.RBNode.lowerBound?_mem_lb {α : Type u_1} {cut : αOrdering} {lb : } {x : α} {t : } (h : Std.RBNode.lowerBound? cut t lb = some x) :
x t x lb
theorem Std.RBNode.lowerBound?_mem {α : Type u_1} {cut : αOrdering} {x : α} {t : } (h : Std.RBNode.lowerBound? cut t none = some x) :
x t
theorem Std.RBNode.lowerBound?_of_some {α : Type u_1} {cut : αOrdering} {y : α} {t : } :
x, Std.RBNode.lowerBound? cut t (some y) = some x
theorem Std.RBNode.Ordered.lowerBound?_exists {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (h : ) :
(x, Std.RBNode.lowerBound? cut t none = some x) x, x t cut x Ordering.lt
theorem Std.RBNode.Ordered.lowerBound?_least_lb {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } {lb : } {x : α} {y : α} [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (h : ) (hlb : ∀ {x : α}, lb = some xStd.RBNode.All (fun x_1 => Std.RBNode.cmpLT cmp x x_1) t) :
Std.RBNode.lowerBound? cut t lb = some xy tcut x = Ordering.gtcmp x y = Ordering.ltcut y = Ordering.lt
theorem Std.RBNode.Ordered.lowerBound?_least {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } {x : α} {y : α} [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (ht : ) (H : Std.RBNode.lowerBound? cut t none = some x) (hy : y t) (xy : cmp x y = Ordering.lt) (hx : cut x = Ordering.gt) :

A statement of the least-ness of the result of lowerBound?. If x is the return value of lowerBound? and it is strictly less than the cut, then any other y > x in the tree is in fact strictly greater than the cut (so there is no exact match, and nothing closer to the cut).

theorem Std.RBNode.Ordered.memP_iff_lowerBound? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] (ht : ) :
theorem Std.RBNode.Ordered.lowerBound?_lt {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } {x : α} {y : α} [Std.TransCmp cmp] [Std.RBNode.IsStrictCut cmp cut] (ht : ) (H : Std.RBNode.lowerBound? cut t none = some x) (hy : y t) :
cmp x y = Ordering.lt cut y = Ordering.lt

A stronger version of lowerBound?_least that holds when the cut is strict.

theorem Std.RBNode.foldr_cons {α : Type u_1} (t : ) (l : List α) :
Std.RBNode.foldr (fun x x_1 => x :: x_1) t l =
@[simp]
theorem Std.RBNode.toList_nil {α : Type u_1} :
Std.RBNode.toList Std.RBNode.nil = []
@[simp]
theorem Std.RBNode.toList_node {α : Type u_1} {c : Std.RBColor} {a : } {x : α} {b : } :
@[simp]
theorem Std.RBNode.mem_toList {α : Type u_1} {x : α} {t : } :
x t
theorem Std.RBNode.foldr_eq_foldr_toList {α : Type u_1} :
∀ {α : Type u_2} {f : ααα} {init : α} {t : }, Std.RBNode.foldr f t init = List.foldr f init ()
theorem Std.RBNode.foldl_eq_foldl_toList {α : Type u_1} :
∀ {α : Type u_2} {f : ααα} {init : α} {t : }, Std.RBNode.foldl f init t = List.foldl f init ()
theorem Std.RBNode.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {f : α} [] [] {t : } :
=
theorem Std.RBNode.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} :
∀ {a : Type u_1} {f : aαm a} {init : a} [inst : ] [inst_1 : ] {t : }, Std.RBNode.foldlM f init t = List.foldlM f init ()
theorem Std.RBNode.forIn_visit_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} :
∀ {α : Type u_1} {f : ααm ()} {init : α} [inst : ] [inst_1 : ] {t : }, Std.RBNode.forIn.visit f t init = ForInStep.bindList f () (ForInStep.yield init)
theorem Std.RBNode.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} :
∀ {α : Type u_1} {init : α} {f : ααm ()} [inst : ] [inst_1 : ] {t : }, forIn t init f = forIn () init f
theorem Std.RBNode.Stream.foldr_cons {α : Type u_1} (t : ) (l : List α) :
Std.RBNode.Stream.foldr (fun x x_1 => x :: x_1) t l =
@[simp]
theorem Std.RBNode.Stream.toList_nil {α : Type u_1} :
Std.RBNode.Stream.toList Std.RBNode.Stream.nil = []
@[simp]
theorem Std.RBNode.Stream.toList_cons {α : Type u_1} {x : α} {r : } {s : } :
theorem Std.RBNode.Stream.foldr_eq_foldr_toList {α : Type u_1} :
∀ {α : Type u_2} {f : ααα} {init : α} {s : }, Std.RBNode.Stream.foldr f s init = List.foldr f init ()
theorem Std.RBNode.Stream.foldl_eq_foldl_toList {α : Type u_1} :
∀ {α : Type u_2} {f : ααα} {init : α} {t : }, Std.RBNode.Stream.foldl f init t = List.foldl f init ()
theorem Std.RBNode.Stream.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} :
∀ {α : Type u_1} {init : α} {f : ααm ()} [inst : ] [inst_1 : ] {t : }, forIn t init f = forIn () init f
theorem Std.RBNode.toStream_toList' {α : Type u_1} {t : } {s : } :
@[simp]
theorem Std.RBNode.toStream_toList {α : Type u_1} {t : } :
theorem Std.RBNode.Stream.next?_toList {α : Type u_1} {s : } :
Option.map (fun x => match x with | (a, b) => (a, )) () =
theorem Std.RBNode.ordered_iff {α : Type u_1} {cmp : ααOrdering} {t : } :
theorem Std.RBNode.Ordered.toList_sorted {α : Type u_1} {cmp : ααOrdering} {t : } :
@[simp]
theorem Std.RBNode.setBlack_toList {α : Type u_1} {t : } :
@[simp]
theorem Std.RBNode.setRed_toList {α : Type u_1} {t : } :
@[simp]
theorem Std.RBNode.balance1_toList {α : Type u_1} {l : } {v : α} {r : } :
@[simp]
theorem Std.RBNode.balance2_toList {α : Type u_1} {l : } {v : α} {r : } :
@[simp]
theorem Std.RBNode.balLeft_toList {α : Type u_1} {l : } {v : α} {r : } :
@[simp]
theorem Std.RBNode.balRight_toList {α : Type u_1} {l : } {v : α} {r : } :
theorem Std.RBNode.size_eq {α : Type u_1} {t : } :
def Std.RBNode.Path.listL {α : Type u_1} :
List α

The list of elements to the left of the hole. (This function is intended for specification purposes only.)

Equations
Instances For
def Std.RBNode.Path.listR {α : Type u_1} :
List α

The list of elements to the right of the hole. (This function is intended for specification purposes only.)

Equations
Instances For
@[inline, reducible]
abbrev Std.RBNode.Path.withList {α : Type u_1} (p : ) (l : List α) :
List α

Wraps a list of elements with the left and right elements of the path.

Instances For
theorem Std.RBNode.Path.rootOrdered_iff {α : Type u_1} {cmp : ααOrdering} {v : α} {p : } (hp : ) :
(∀ (a : α), Std.RBNode.cmpLT cmp a v) ∀ (a : α), Std.RBNode.cmpLT cmp v a
theorem Std.RBNode.Path.ordered_iff {α : Type u_1} {cmp : ααOrdering} {p : } :
∀ (x : α), ∀ (y : α), Std.RBNode.cmpLT cmp x y
@[simp]
theorem Std.RBNode.Path.fill_toList {α : Type u_1} {t : } {p : } :
theorem Std.RBNode.zoom_toList {α : Type u_1} {cut : αOrdering} {t' : } {p' : } {t : } (eq : Std.RBNode.zoom cut t Std.RBNode.Path.root = (t', p')) :
@[simp]
theorem Std.RBNode.Path.ins_toList {α : Type u_1} {t : } {p : } :
@[simp]
theorem Std.RBNode.Path.insertNew_toList {α : Type u_1} {v : α} {p : } :
theorem Std.RBNode.Path.insert_toList {α : Type u_1} {t : } {v : α} {p : } :
theorem Std.RBNode.insert_toList_zoom {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {t' : } {p : } {v : α} {t : } (ht : ) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (t', p)) :
theorem Std.RBNode.insert_toList_zoom_nil {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {p : } {v : α} {t : } (ht : ) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.nil, p)) :
theorem Std.RBNode.exists_insert_toList_zoom_nil {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {p : } {v : α} {t : } (ht : ) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.nil, p)) :
L R, = L ++ R Std.RBNode.toList (Std.RBNode.insert cmp t v) = L ++ v :: R
theorem Std.RBNode.insert_toList_zoom_node {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {c' : Std.RBColor} {l : } {v' : α} {r : } {p : } {v : α} {t : } (ht : ) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.node c' l v' r, p)) :
theorem Std.RBNode.exists_insert_toList_zoom_node {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {c' : Std.RBColor} {l : } {v' : α} {r : } {p : } {v : α} {t : } (ht : ) (e : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.node c' l v' r, p)) :
L R, = L ++ v' :: R Std.RBNode.toList (Std.RBNode.insert cmp t v) = L ++ v :: R
theorem Std.RBNode.mem_insert_self {α : Type u_1} {c : Std.RBColor} {n : Nat} {v : α} {cmp : ααOrdering} {t : } (ht : ) :
theorem Std.RBNode.mem_insert_of_mem {α : Type u_1} {c : Std.RBColor} {n : Nat} {v' : α} {cmp : ααOrdering} {v : α} {t : } (ht : ) (h : v' t) :
v' Std.RBNode.insert cmp t v cmp v v' = Ordering.eq
theorem Std.RBNode.exists_find?_insert_self {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {c : Std.RBColor} {n : Nat} {v : α} [Std.TransCmp cmp] [Std.RBNode.IsCut cmp cut] {t : } (ht : ) (ht₂ : ) (hv : cut v = Ordering.eq) :
x, Std.RBNode.find? cut (Std.RBNode.insert cmp t v) = some x
theorem Std.RBNode.find?_insert_self {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {c : Std.RBColor} {n : Nat} {v : α} [Std.TransCmp cmp] [Std.RBNode.IsStrictCut cmp cut] {t : } (ht : ) (ht₂ : ) (hv : cut v = Ordering.eq) :
theorem Std.RBNode.mem_insert {α : Type u_1} {cmp : ααOrdering} {c : Std.RBColor} {n : Nat} {v' : α} {v : α} [Std.TransCmp cmp] {t : } (ht : ) (ht₂ : ) :
v' Std.RBNode.insert cmp t v v' t Std.RBNode.find? (cmp v) t some v' v' = v
@[simp]
theorem Std.RBSet.val_toList {α : Type u_1} {cmp : ααOrdering} {t : Std.RBSet α cmp} :
@[simp]
theorem Std.RBSet.mkRBSet_eq {α : Type u_1} {cmp : ααOrdering} :
@[simp]
theorem Std.RBSet.empty_eq {α : Type u_1} {cmp : ααOrdering} :
Std.RBSet.empty =
@[simp]
theorem Std.RBSet.default_eq {α : Type u_1} {cmp : ααOrdering} :
default =
@[simp]
theorem Std.RBSet.empty_toList {α : Type u_1} {cmp : ααOrdering} :
@[simp]
theorem Std.RBSet.single_toList {α : Type u_1} {cmp : ααOrdering} {a : α} :
theorem Std.RBSet.mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Std.RBSet α cmp} :
x t.val
theorem Std.RBSet.mem_congr {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} (h : cmp x y = Ordering.eq) :
x t y t
theorem Std.RBSet.mem_iff_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Std.RBSet α cmp} :
x t y, cmp x y = Ordering.eq
theorem Std.RBSet.mem_of_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} [] {t : Std.RBSet α cmp} (h : ) :
x t
theorem Std.RBSet.foldl_eq_foldl_toList {α : Type u_1} {cmp : ααOrdering} :
∀ {α : Type u_2} {f : ααα} {init : α} {t : Std.RBSet α cmp}, Std.RBSet.foldl f init t = List.foldl f init ()
theorem Std.RBSet.foldr_eq_foldr_toList {α : Type u_1} {cmp : ααOrdering} :
∀ {α : Type u_2} {f : ααα} {init : α} {t : Std.RBSet α cmp}, Std.RBSet.foldr f init t = List.foldr f init ()
theorem Std.RBSet.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} :
∀ {a : Type u_1} {f : aαm a} {init : a} [inst : ] [inst_1 : ] {t : Std.RBSet α cmp}, Std.RBSet.foldlM f init t = List.foldlM f init ()
theorem Std.RBSet.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} :
∀ {α : Type u_1} {init : α} {f : ααm ()} [inst : ] [inst_1 : ] {t : Std.RBSet α cmp}, forIn t init f = forIn () init f
theorem Std.RBSet.toStream_eq {α : Type u_1} {cmp : ααOrdering} {t : Std.RBSet α cmp} :
= Std.RBNode.toStream t.val Std.RBNode.Stream.nil
@[simp]
theorem Std.RBSet.toStream_toList {α : Type u_1} {cmp : ααOrdering} {t : Std.RBSet α cmp} :
theorem Std.RBSet.toList_sorted {α : Type u_1} {cmp : ααOrdering} {t : Std.RBSet α cmp} :
theorem Std.RBSet.find?_some_eq_eq {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Std.RBSet α cmp} :
= some ycmp x y = Ordering.eq
theorem Std.RBSet.find?_some_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Std.RBSet α cmp} (h : = some y) :
theorem Std.RBSet.find?_some_mem {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Std.RBSet α cmp} (h : = some y) :
x t
theorem Std.RBSet.mem_toList_unique {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} (hx : ) (hy : ) (e : cmp x y = Ordering.eq) :
x = y
theorem Std.RBSet.find?_some {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :
= some y cmp x y = Ordering.eq
theorem Std.RBSet.mem_iff_find? {α : Type u_1} {cmp : ααOrdering} {x : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :
x t y, = some y
@[simp]
theorem Std.RBSet.contains_iff {α : Type u_1} {cmp : ααOrdering} {x : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :
x t
instance Std.RBSet.instDecidableMemRBSetInstMembershipRBSet {α : Type u_1} {cmp : ααOrdering} {x : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :
theorem Std.RBSet.size_eq {α : Type u_1} {cmp : ααOrdering} (t : Std.RBSet α cmp) :
theorem Std.RBSet.mem_toList_insert_self {α : Type u_1} {cmp : ααOrdering} (v : α) (t : Std.RBSet α cmp) :
theorem Std.RBSet.mem_insert_self {α : Type u_1} {cmp : ααOrdering} [] (v : α) (t : Std.RBSet α cmp) :
v
theorem Std.RBSet.mem_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {v : α} {v' : α} [Std.TransCmp cmp] (t : Std.RBSet α cmp) (h : cmp v v' = Ordering.eq) :
v'
theorem Std.RBSet.mem_toList_insert_of_mem {α : Type u_1} {cmp : ααOrdering} {v' : α} (v : α) {t : Std.RBSet α cmp} (h : ) :
v' cmp v v' = Ordering.eq
theorem Std.RBSet.mem_insert_of_mem_toList {α : Type u_1} {cmp : ααOrdering} {v' : α} [] (v : α) {t : Std.RBSet α cmp} (h : ) :
v'
theorem Std.RBSet.mem_insert_of_mem {α : Type u_1} {cmp : ααOrdering} {v' : α} [Std.TransCmp cmp] (v : α) {t : Std.RBSet α cmp} (h : v' t) :
v'
theorem Std.RBSet.mem_toList_insert {α : Type u_1} {cmp : ααOrdering} {v' : α} {v : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :
v' some v' v' = v
theorem Std.RBSet.mem_insert {α : Type u_1} {cmp : ααOrdering} {v' : α} {v : α} [Std.TransCmp cmp] {t : Std.RBSet α cmp} :
v' v' t cmp v v' = Ordering.eq
theorem Std.RBSet.find?_congr {α : Type u_1} {cmp : ααOrdering} {v₁ : α} {v₂ : α} [Std.TransCmp cmp] (t : Std.RBSet α cmp) (h : cmp v₁ v₂ = Ordering.eq) :
=
theorem Std.RBSet.find?_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {v' : α} {v : α} [Std.TransCmp cmp] (t : Std.RBSet α cmp) (h : cmp v' v = Ordering.eq) :
theorem Std.RBSet.find?_insert_of_ne {α : Type u_1} {cmp : ααOrdering} {v' : α} {v : α} [Std.TransCmp cmp] (t : Std.RBSet α cmp) (h : cmp v' v Ordering.eq) :
theorem Std.RBSet.find?_insert {α : Type u_1} {cmp : ααOrdering} [Std.TransCmp cmp] (t : Std.RBSet α cmp) (v : α) (v' : α) :
Std.RBSet.find? () v' = if cmp v' v = Ordering.eq then some v else