mathlib 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.ltp lp (l.red_node y r)) (h₃ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.eqp (l.red_node y r)) (h₄ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.gtp rp (l.red_node y r)) (h₅ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.ltp lp (l.black_node y r)) (h₆ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.eqp (l.black_node y r)) (h₇ : ∀ (l : rbnode α) (y : α) (r : rbnode α), cmp_using lt x y = ordering.gtp rp (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 = some y strict_weak_order.equiv x y
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 = 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