English
There is a nonrecursive insertion operation insert' that places x into Ordset α with balanced BST-style balancing, running in O(log n) time; if x is already present, the set is returned unchanged.
Русский
Существует нерекурсивная вставка insert', которая вставляет элемент x в Ordset α с балансировкой в духе сбалансированного BST и выполняется за O(log n); если x уже присутствует, множество не изменяется.
LaTeX
$$$$ \\mathrm{insert'}(x,s)=\\mathrm{Ordset.insert}(x,s). $$$$
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, the set is returned as is. -/
nonrec def insert' [IsTotal α (· ≤ ·)] [DecidableLE α] (x : α) (s : Ordset α) : Ordset α :=
⟨insert' x s.1, insert'.valid _ s.2⟩
