English
There is a function splitMin which, for a nonempty tree, returns the minimum element together with the remaining tree; for the empty tree it returns none.
Русский
Существует функция splitMin, которая для непустого дерева возвращает минимальный элемент и оставшееся дерево; для пустого дерева возвращает none.
LaTeX
$$$$ \mathrm{splitMin}: \ Ordnode\; \alpha \to \mathrm{Option}(\ Ordnode\; \alpha \times \alpha ), \\ \mathrm{splitMin}(nil) = \mathrm{none}, \\ \mathrm{splitMin}(\mathrm{node}\; - \; l \; x \; r) = \mathrm{splitMin'}(l, x, r) $$$$
Lean4
/-- O(log n). Extract and remove the minimum element from the tree, if it exists.
split_min {1, 2, 3} = some (1, {2, 3})
split_min ∅ = none -/
def splitMin : Ordnode α → Option (α × Ordnode α)
| nil => none
| node _ l x r => splitMin' l x r
