mathlib documentation

data.rbtree.main

theorem rbnode.is_searchable_of_well_formed {α : Type u} {lt : α → α → Prop} {t : rbnode α} [is_strict_weak_order α lt] :
theorem rbnode.is_red_black_of_well_formed {α : Type u} {lt : α → α → Prop} {t : rbnode α} :
rbnode.well_formed lt t(∃ (c : rbnode.color) (n : ), t.is_red_black c n)
theorem rbtree.balanced {α : Type u} {lt : α → α → Prop} (t : rbtree α lt) :
theorem rbtree.not_mem_mk_rbtree {α : Type u} {lt : α → α → Prop} (a : α) :
a mk_rbtree α lt
theorem rbtree.not_mem_of_empty {α : Type u} {lt : α → α → Prop} {t : rbtree α lt} (a : α) :
t.empty = tta t
theorem rbtree.mem_of_mem_of_eqv {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {t : rbtree α lt} {a b : α} :
a tstrict_weak_order.equiv a bb t
theorem rbtree.insert_ne_mk_rbtree {α : Type u} {lt : α → α → Prop} [decidable_rel lt] (t : rbtree α lt) (a : α) :
t.insert a mk_rbtree α lt
theorem rbtree.find_correct {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (a : α) (t : rbtree α lt) :
a t ∃ (b : α), t.find a = some b strict_weak_order.equiv a b
theorem rbtree.find_correct_of_total {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] (a : α) (t : rbtree α lt) :
a t t.find a = some a
theorem rbtree.find_correct_exact {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] (a : α) (t : rbtree α lt) :
theorem rbtree.find_insert_of_eqv {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (t : rbtree α lt) {x y : α} :
theorem rbtree.find_insert {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (t : rbtree α lt) (x : α) :
(t.insert x).find x = some x
theorem rbtree.find_insert_of_disj {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {x y : α} (t : rbtree α lt) :
lt x y lt y x(t.insert x).find y = t.find y
theorem rbtree.find_insert_of_not_eqv {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {x y : α} (t : rbtree α lt) :
theorem rbtree.find_insert_of_ne {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {x y : α} (t : rbtree α lt) :
x y(t.insert x).find y = t.find y
theorem rbtree.not_mem_of_find_none {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a : α} {t : rbtree α lt} :
t.find a = nonea t
theorem rbtree.eqv_of_find_some {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a b : α} {t : rbtree α lt} :
theorem rbtree.eq_of_find_some {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {a b : α} {t : rbtree α lt} :
t.find a = some ba = b
theorem rbtree.mem_of_find_some {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a b : α} {t : rbtree α lt} :
t.find a = some ba t
theorem rbtree.find_eq_find_of_eqv {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a b : α} (t : rbtree α lt) :
theorem rbtree.contains_correct {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (a : α) (t : rbtree α lt) :
a t t.contains a = tt
theorem rbtree.mem_insert_of_incomp {α : Type u} {lt : α → α → Prop} [decidable_rel lt] {a b : α} (t : rbtree α lt) :
¬lt a b ¬lt b aa t.insert b
theorem rbtree.mem_insert {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_irrefl α lt] (a : α) (t : rbtree α lt) :
a t.insert a
theorem rbtree.mem_insert_of_equiv {α : Type u} {lt : α → α → Prop} [decidable_rel lt] {a b : α} (t : rbtree α lt) :
theorem rbtree.mem_insert_of_mem {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a : α} {t : rbtree α lt} (b : α) :
a ta t.insert b
theorem rbtree.equiv_or_mem_of_mem_insert {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a b : α} {t : rbtree α lt} :
theorem rbtree.incomp_or_mem_of_mem_ins {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a b : α} {t : rbtree α lt} :
a t.insert b¬lt a b ¬lt b a a t
theorem rbtree.eq_or_mem_of_mem_ins {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] {a b : α} {t : rbtree α lt} :
a t.insert ba = b a t
theorem rbtree.mem_of_min_eq {α : Type u} {lt : α → α → Prop} [is_irrefl α lt] {a : α} {t : rbtree α lt} :
t.min = some aa t
theorem rbtree.mem_of_max_eq {α : Type u} {lt : α → α → Prop} [is_irrefl α lt] {a : α} {t : rbtree α lt} :
t.max = some aa t
theorem rbtree.eq_leaf_of_min_eq_none {α : Type u} {lt : α → α → Prop} {t : rbtree α lt} :
t.min = nonet = mk_rbtree α lt
theorem rbtree.eq_leaf_of_max_eq_none {α : Type u} {lt : α → α → Prop} {t : rbtree α lt} :
t.max = nonet = mk_rbtree α lt
theorem rbtree.min_is_minimal {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {a : α} {t : rbtree α lt} :
t.min = some a∀ {b : α}, b tstrict_weak_order.equiv a b lt a b
theorem rbtree.max_is_maximal {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {a : α} {t : rbtree α lt} :
t.max = some a∀ {b : α}, b tstrict_weak_order.equiv a b lt b a