mathlib3 documentation

data.rbtree.main

theorem rbnode.is_searchable_of_well_formed {α : Type u} {lt : α → α → Prop} {t : rbnode α} [is_strict_weak_order α lt] :

rbnode.well_formed lt t → rbnode.is_searchable lt t option.none option.none

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) :

rbtree.depth linear_order.max t ≤ 2 * rbtree.depth linear_order.min t + 1

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 = bool.tt → a ∉ t

theorem rbtree.mem_of_mem_of_eqv {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {t : rbtree α lt} {a b : α} :

a ∈ t → strict_weak_order.equiv a b → b ∈ 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 = option.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 = option.some a

theorem rbtree.find_correct_exact {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_total_order α lt] (a : α) (t : rbtree α lt) :

rbtree.mem_exact a t ↔ t.find a = option.some a

theorem rbtree.find_insert_of_eqv {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] (t : rbtree α lt) {x y : α} :

strict_weak_order.equiv x y → (t.insert x).find y = option.some x

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 = option.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) :

¬strict_weak_order.equiv x y → (t.insert x).find y = t.find y

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 = option.none → a ∉ t

theorem rbtree.eqv_of_find_some {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a b : α} {t : rbtree α lt} :

t.find a = option.some b → strict_weak_order.equiv a b

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 = option.some b → a = 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 = option.some b → a ∈ 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) :

strict_weak_order.equiv a b → t.find a = t.find b

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 = bool.tt

theorem rbtree.mem_insert_of_incomp {α : Type u} {lt : α → α → Prop} [decidable_rel lt] {a b : α} (t : rbtree α lt) :

¬lt a b ∧ ¬lt b a → a ∈ 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) :

strict_weak_order.equiv a b → a ∈ t.insert b

theorem rbtree.mem_insert_of_mem {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_weak_order α lt] {a : α} {t : rbtree α lt} (b : α) :

a ∈ t → a ∈ t.insert b

theorem rbtree.equiv_or_mem_of_mem_insert {α : Type u} {lt : α → α → Prop} [decidable_rel lt] {a b : α} {t : rbtree α lt} :

a ∈ t.insert b → strict_weak_order.equiv a b ∨ a ∈ t

theorem rbtree.incomp_or_mem_of_mem_ins {α : Type u} {lt : α → α → Prop} [decidable_rel 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 b → a = b ∨ a ∈ t

theorem rbtree.mem_of_min_eq {α : Type u} {lt : α → α → Prop} [is_irrefl α lt] {a : α} {t : rbtree α lt} :

t.min = option.some a → a ∈ t

theorem rbtree.mem_of_max_eq {α : Type u} {lt : α → α → Prop} [is_irrefl α lt] {a : α} {t : rbtree α lt} :

t.max = option.some a → a ∈ t

theorem rbtree.eq_leaf_of_min_eq_none {α : Type u} {lt : α → α → Prop} {t : rbtree α lt} :

t.min = option.none → t = mk_rbtree α lt

theorem rbtree.eq_leaf_of_max_eq_none {α : Type u} {lt : α → α → Prop} {t : rbtree α lt} :

t.max = option.none → t = mk_rbtree α lt

theorem rbtree.min_is_minimal {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {a : α} {t : rbtree α lt} :

t.min = option.some a → ∀ {b : α}, b ∈ t → strict_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 = option.some a → ∀ {b : α}, b ∈ t → strict_weak_order.equiv a b ∨ lt b a