mathlib3 documentation

data.rbtree.min_max

theorem rbnode.mem_of_min_eq {α : Type u} (lt : α α Prop) [is_irrefl α lt] {a : α} {t : rbnode α} :
theorem rbnode.mem_of_max_eq {α : Type u} (lt : α α Prop) [is_irrefl α lt] {a : α} {t : rbnode α} :
theorem rbnode.min_is_minimal {α : Type u} {lt : α α Prop} [is_strict_weak_order α lt] {a : α} {t : rbnode α} {lo hi : option α} :
theorem rbnode.max_is_maximal {α : Type u} {lt : α α Prop} [is_strict_weak_order α lt] {a : α} {t : rbnode α} {lo hi : option α} :