English
There is a map operation across Ordset α to Ordset β, using a function f that is StrictMono (order-preserving). The operation preserves the tree structure and yields a valid Ordset β.
Русский
Существует отображение Ordset α в Ordset β, задаваемое функцией f, которая строго монотонна и сохраняет структуру дерева; результат является валидным Ordset β.
LaTeX
$$$$ \\mathrm{map}: (f:\\alpha\\to\\beta),\\ \\text{StrictMono}(f) \\to \\mathrm{Ordset}(\\alpha)\\to \\mathrm{Ordset}(\\beta). $$$$
Lean4
/-- O(n). Map a function across a tree, without changing the structure. -/
def map {β} [Preorder β] (f : α → β) (f_strict_mono : StrictMono f) (s : Ordset α) : Ordset β :=
⟨Ordnode.map f s.val, Ordnode.map.valid f_strict_mono s.property⟩
