mathlib3 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 a → rbnode.mem lt a t

theorem rbnode.mem_of_max_eq {α : Type u} (lt : α → α → Prop) [is_irrefl α lt] {a : α} {t : rbnode α} :

t.max = option.some a → rbnode.mem lt a t

theorem rbnode.eq_leaf_of_min_eq_none {α : Type u} {t : rbnode α} :

t.min = option.none → t = rbnode.leaf

theorem rbnode.eq_leaf_of_max_eq_none {α : Type u} {t : rbnode α} :

t.max = option.none → t = rbnode.leaf

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 hi → t.min = option.some a → ∀ {b : α}, rbnode.mem lt b t → strict_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 hi → t.max = option.some a → ∀ {b : α}, rbnode.mem lt b t → strict_weak_order.equiv a b ∨ lt b a