Equations
- rbnode.lift lt (option.some a) (option.some b) = lt a b
- rbnode.lift lt (option.some val) option.none = true
- rbnode.lift lt option.none _x = true
- leaf_s : ∀ {α : Type u} {lt : α → α → Prop} {lo hi : option α}, rbnode.lift lt lo hi → rbnode.is_searchable lt rbnode.leaf lo hi
- red_s : ∀ {α : Type u} {lt : α → α → Prop} {l r : rbnode α} {v : α} {lo hi : option α}, rbnode.is_searchable lt l lo (option.some v) → rbnode.is_searchable lt r (option.some v) hi → rbnode.is_searchable lt (l.red_node v r) lo hi
- black_s : ∀ {α : Type u} {lt : α → α → Prop} {l r : rbnode α} {v : α} {lo hi : option α}, rbnode.is_searchable lt l lo (option.some v) → rbnode.is_searchable lt r (option.some v) hi → rbnode.is_searchable lt (l.black_node v r) lo hi
theorem
rbnode.lo_lt_hi
{α : Type u}
{t : rbnode α}
{lt : α → α → Prop}
[is_trans α lt]
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → rbnode.lift lt lo hi
theorem
rbnode.is_searchable_of_is_searchable_of_incomp
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{t : rbnode α}
{lo : option α}
{hi hi' : α}
(hc : ¬lt hi' hi ∧ ¬lt hi hi')
(hs : rbnode.is_searchable lt t lo (option.some hi)) :
rbnode.is_searchable lt t lo (option.some hi')
theorem
rbnode.is_searchable_of_incomp_of_is_searchable
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{t : rbnode α}
{lo lo' : α}
{hi : option α}
(hc : ¬lt lo' lo ∧ ¬lt lo lo')
(hs : rbnode.is_searchable lt t (option.some lo) hi) :
rbnode.is_searchable lt t (option.some lo') hi
theorem
rbnode.is_searchable_some_low_of_is_searchable_of_lt
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
[is_trans α lt]
{lo : α}
{hi : option α}
{lo' : α}
(hlt : lt lo' lo)
(hs : rbnode.is_searchable lt t (option.some lo) hi) :
rbnode.is_searchable lt t (option.some lo') hi
theorem
rbnode.is_searchable_none_low_of_is_searchable_some_low
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
{y : α}
{hi : option α}
(hlt : rbnode.is_searchable lt t (option.some y) hi) :
rbnode.is_searchable lt t option.none hi
theorem
rbnode.is_searchable_some_high_of_is_searchable_of_lt
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
[is_trans α lt]
{lo : option α}
{hi hi' : α}
(hlt : lt hi hi')
(hs : rbnode.is_searchable lt t lo (option.some hi)) :
rbnode.is_searchable lt t lo (option.some hi')
theorem
rbnode.is_searchable_none_high_of_is_searchable_some_high
{α : Type u}
{lt : α → α → Prop}
{t : rbnode α}
{lo : option α}
{y : α}
(hlt : rbnode.is_searchable lt t lo (option.some y)) :
rbnode.is_searchable lt t lo option.none
theorem
rbnode.range
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{t : rbnode α}
{x : α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → rbnode.mem lt x t → rbnode.lift lt lo (option.some x) ∧ rbnode.lift lt (option.some x) hi
theorem
rbnode.lt_of_mem_left
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{y : α}
{t l r : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → t.is_node_of l y r → ∀ {x : α}, rbnode.mem lt x l → lt x y
theorem
rbnode.lt_of_mem_right
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{y : α}
{t l r : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → t.is_node_of l y r → ∀ {z : α}, rbnode.mem lt z r → lt y z
theorem
rbnode.lt_of_mem_left_right
{α : Type u}
{lt : α → α → Prop}
[is_strict_weak_order α lt]
{y : α}
{t l r : rbnode α}
{lo hi : option α} :
rbnode.is_searchable lt t lo hi → t.is_node_of l y r → ∀ {x z : α}, rbnode.mem lt x l → rbnode.mem lt z r → lt x z
- leaf_rb : ∀ {α : Type u}, rbnode.leaf.is_red_black rbnode.color.black 0
- red_rb : ∀ {α : Type u} {v : α} {l r : rbnode α} {n : ℕ}, l.is_red_black rbnode.color.black n → r.is_red_black rbnode.color.black n → (l.red_node v r).is_red_black rbnode.color.red n
- black_rb : ∀ {α : Type u} {v : α} {l r : rbnode α} {n : ℕ} {c₁ c₂ : rbnode.color}, l.is_red_black c₁ n → r.is_red_black c₂ n → (l.black_node v r).is_red_black rbnode.color.black n.succ
theorem
rbnode.depth_min
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α} :
t.is_red_black c n → n ≤ rbnode.depth linear_order.min t
theorem
rbnode.depth_max'
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α} :
t.is_red_black c n → rbnode.depth linear_order.max t ≤ upper c n
theorem
rbnode.depth_max
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α}
(h : t.is_red_black c n) :
rbnode.depth linear_order.max t ≤ 2 * n + 1
theorem
rbnode.balanced
{α : Type u}
{c : rbnode.color}
{n : ℕ}
{t : rbnode α}
(h : t.is_red_black c n) :