# 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.

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For