theorem
rbnode.find.induction
{α : Type u}
{p : rbnode α → Prop}
(lt : α → α → Prop)
[decidable_rel lt]
(t : rbnode α)
(x : α)
(h₁ : p rbnode.leaf)
(h₂ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.lt → p l → p (l.red_node y r))
(h₃ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.eq → p (l.red_node y r))
(h₄ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.gt → p r → p (l.red_node y r))
(h₅ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.lt → p l → p (l.black_node y r))
(h₆ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.eq → p (l.black_node y r))
(h₇ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.gt → p r → p (l.black_node y r)) :
p t
theorem
rbnode.find_correct
{α : Type u}
{t : rbnode α}
{lt : α → α → Prop}
{x : α}
[decidable_rel lt]
[is_strict_weak_order α lt]
{lo hi : option α}
(hs : rbnode.is_searchable lt t lo hi) :
rbnode.mem lt x t ↔ ∃ (y : α), rbnode.find lt t x = option.some y ∧ strict_weak_order.equiv x y
theorem
rbnode.mem_of_mem_exact
{α : Type u}
{lt : α → α → Prop}
[is_irrefl α lt]
{x : α}
{t : rbnode α} :
rbnode.mem_exact x t → rbnode.mem lt x t
theorem
rbnode.find_correct_exact
{α : Type u}
{t : rbnode α}
{lt : α → α → Prop}
{x : α}
[decidable_rel lt]
[is_strict_weak_order α lt]
{lo hi : option α}
(hs : rbnode.is_searchable lt t lo hi) :
rbnode.mem_exact x t ↔ rbnode.find lt t x = option.some x
theorem
rbnode.eqv_of_find_some
{α : Type u}
{t : rbnode α}
{lt : α → α → Prop}
{x y : α}
[decidable_rel lt]
{lo hi : option α}
(hs : rbnode.is_searchable lt t lo hi)
(he : rbnode.find lt t x = option.some y) :
theorem
rbnode.find_eq_find_of_eqv
{α : Type u}
{lt : α → α → Prop}
{a b : α}
[decidable_rel lt]
[is_strict_weak_order α lt]
{t : rbnode α}
{lo hi : option α}
(hs : rbnode.is_searchable lt t lo hi)
(heqv : strict_weak_order.equiv a b) :
rbnode.find lt t a = rbnode.find lt t b