English
An Ordset α is a finite set of α, represented as an ordered tree with a validity predicate.
Русский
Ordset α есть конечное множество значений α, представленное как упорядоченное дерево с доказательством валидности.
LaTeX
$$$\\mathrm{Ordset}(\\alpha) = \\{ t : \\mathrm{Ordnode}(\\alpha) \\mid t.\\mathrm{Valid} \\}$$$
Lean4
/-- An `Ordset α` is a finite set of values, represented as a tree. The operations on this type
maintain that the tree is balanced and correctly stores subtree sizes at each level. The
correctness property of the tree is baked into the type, so all operations on this type are correct
by construction. -/
def Ordset (α : Type*) [Preorder α] :=
{ t : Ordnode α // t.Valid }
