mathlib documentation

data.rbtree.min_max

theorem rbnode.mem_of_min_eq {α : Type u} (lt : α → α → Prop) [is_irrefl α lt] {a : α} {t : rbnode α} :
t.min = option.some arbnode.mem lt a t
theorem rbnode.mem_of_max_eq {α : Type u} (lt : α → α → Prop) [is_irrefl α lt] {a : α} {t : rbnode α} :
t.max = option.some arbnode.mem lt a t
theorem rbnode.eq_leaf_of_min_eq_none {α : Type u} {t : rbnode α} :
theorem rbnode.eq_leaf_of_max_eq_none {α : Type u} {t : rbnode α} :
theorem rbnode.min_is_minimal {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {a : α} {t : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt t lo hit.min = option.some a∀ {b : α}, rbnode.mem lt b tstrict_weak_order.equiv a b lt a b
theorem rbnode.max_is_maximal {α : Type u} {lt : α → α → Prop} [is_strict_weak_order α lt] {a : α} {t : rbnode α} {lo hi : option α} :
rbnode.is_searchable lt t lo hit.max = option.some a∀ {b : α}, rbnode.mem lt b tstrict_weak_order.equiv a b lt b a