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.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 : α) :
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) :
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) :
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) :
theorem
rbtree.mem_insert
{α : Type u}
{lt : α → α → Prop}
[decidable_rel lt]
[is_irrefl α lt]
(a : α)
(t : rbtree α lt) :
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 : α) :
theorem
rbtree.equiv_or_mem_of_mem_insert
{α : Type u}
{lt : α → α → Prop}
[decidable_rel lt]
{a b : α}
{t : rbtree α lt} :
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} :
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