mathlib3 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 α} :
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 α} :
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
inductive rbnode.is_red_black {α : Type u} :
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) :