Additional tree set operations

This file defines more operations on Std.TreeSet. We currently do not provide lemmas for these functions.

We do not provide get*GE, get*GT, get*LE and get*LT functions for the raw trees.

@[inline]

def Std.TreeSet.getGE {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isGE = true) : α

Given a proof that such an element exists, retrieves the smallest element that is greater than or equal to the given element.

Equations

• t.getGE k h = t.inner.getKeyGE k h

@[inline]

def Std.TreeSet.getGT {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : α

Given a proof that such an element exists, retrieves the smallest element that is greater than the given element.

Equations

• t.getGT k h = t.inner.getKeyGT k h

@[inline]

def Std.TreeSet.getLE {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isLE = true) : α

Given a proof that such an element exists, retrieves the largest element that is less than or equal to the given element.

Equations

• t.getLE k h = t.inner.getKeyLE k h

@[inline]

def Std.TreeSet.getLT {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : TreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : α

Given a proof that such an element exists, retrieves the smallest element that is less than the given element.

Equations

• t.getLT k h = t.inner.getKeyLT k h