English
Inserting an element into an Ordset preserves balance and BST property; if the element already exists, it replaces it.
Русский
Вставка элемента в Ordset сохраняет баланс и свойство BST; если элемент уже существует, он заменяется.
LaTeX
$$$\\text{Ordset.insert}(x,s) \\in \\mathrm{Ordset}(\\alpha)$ and preserves BST invariants$$
Lean4
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, this replaces it. -/
protected def insert [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) (s : Ordset α) : Ordset α :=
⟨Ordnode.insert x s.1, insert.valid _ s.2⟩
