mathlib3 documentation

data.rbtree.find

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) :
theorem rbnode.mem_of_mem_exact {α : Type u} {lt : α α Prop} [is_irrefl α lt] {x : α} {t : rbnode α} :
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) :
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