English
There is an erase operation that removes an element equivalent to x from Ordset α in logarithmic time; if x is not present, the set remains unchanged.
Русский
Существует операция erase, удаляющая элемент, эквивалентный x, из Ordset α заO(log n); если такого элемента нет, множество не меняется.
LaTeX
$$$$ \\mathrm{erase}(x,s)=\\begin{cases} \\text{Ordnode.erase}(x,s.1) & \\text{in underlying tree}\\,, \\\\ \\mathrm{Ordnode.erase.valid}(x,s.2) &\\text{validity}\\end{cases} $$$$
Lean4
/-- O(log n). Remove an element from the set equivalent to `x`. Does nothing if there
is no such element. -/
def erase [DecidableLE α] (x : α) (s : Ordset α) : Ordset α :=
⟨Ordnode.erase x s.val, Ordnode.erase.valid x s.property⟩
