English
Bounded(t, lo, hi) expresses that every element in t lies strictly between lo and hi, and this property holds recursively in the subtrees, making the whole tree a binary search tree. If t is nil, it holds trivially.
Русский
Bounded(t, lo, hi) означает, что каждый элемент дерева t лежит строго между lo и hi, и это свойство рекурсивно распространяется на поддеревья, образуя двоичное дерево поиска. Если дерево пусто, свойство выполняется тривиально.
LaTeX
$$$\text{Bounded}:\ Ordnode\ α\to\WithBot\ α\to\WithTop\ α\to\text{Prop}$ defined by\nBounded(nil, o_1, o_2) = True,\nBounded(node\ l\ x\ r, o_1, o_2) = Bounded(l, o_1, x) \wedge Bounded(r, x, o_2)$$
Lean4
/-- `Bounded t lo hi` says that every element `x ∈ t` is in the range `lo < x < hi`, and also this
property holds recursively in subtrees, making the full tree a BST. The bounds can be set to
`lo = ⊥` and `hi = ⊤` if we care only about the internal ordering constraints. -/
def Bounded : Ordnode α → WithBot α → WithTop α → Prop
| nil, some a, some b => a < b
| nil, _, _ => True
| node _ l x r, o₁, o₂ => Bounded l o₁ x ∧ Bounded r (↑x) o₂
