mathlib documentation

data.rbtree.basic

inductive rbnode.is_node_of {α : Type u} :
rbnode αrbnode αα → rbnode α → Prop
def rbnode.lift {α : Type u} (lt : α → α → Prop) :
option αoption α → Prop
Equations
inductive rbnode.is_searchable {α : Type u} (lt : α → α → Prop) :
rbnode αoption αoption α → Prop
theorem rbnode.lo_lt_hi {α : Type u} {t : rbnode α} {lt : α → α → Prop} [is_trans α lt] {lo hi : option α} :
rbnode.is_searchable lt t lo hirbnode.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)) :
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) :
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) :
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) :
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)) :
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)) :
theorem rbnode.range {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {t : rbnode α} {x : α} {lo hi : option α} :
rbnode.is_searchable lt t lo hirbnode.mem lt x trbnode.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 hit.is_node_of l y r∀ {x : α}, rbnode.mem lt x llt 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 hit.is_node_of l y r∀ {z : α}, rbnode.mem lt z rlt 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 hit.is_node_of l y r∀ {x z : α}, rbnode.mem lt x lrbnode.mem lt z rlt x z
inductive rbnode.is_red_black {α : Type u} :
rbnode αrbnode.color → Prop
theorem rbnode.depth_min {α : Type u} {c : rbnode.color} {n : } {t : rbnode α} :
theorem rbnode.depth_max' {α : Type u} {c : rbnode.color} {n : } {t : rbnode α} :
theorem rbnode.depth_max {α : Type u} {c : rbnode.color} {n : } {t : rbnode α} (h : t.is_red_black c n) :
theorem rbnode.balanced {α : Type u} {c : rbnode.color} {n : } {t : rbnode α} (h : t.is_red_black c n) :