English
O(m + n). Build a set on the disjoint union by combining trees on the factors. An element from the left tree is wrapped with Inl, an element from the right tree with Inr.
Русский
O(m + n). Построить множество на дизъюнкции по объединению деревьев слева и справа, помечая элементы иньк.\n
LaTeX
$$$$ \\mathrm{copair}: (t_1 : Ordnode\\; \\alpha) \\to (t_2 : Ordnode\\; \\beta) \\to Ordnode\\; (\\alpha \\oplus \\beta), \\quad \\mathrm{copair}(t_1,t_2) = \\mathrm{merge}(\\mathrm{map}\\;\\mathrm{Sum.inl}\ t_1)\, (\\mathrm{map}\\;\\mathrm{Sum.inr}\ t_2) $$$$
Lean4
/-- O(m + n). Build a set on the disjoint union by combining sets on the factors.
`Or.inl a ∈ s.copair t` iff `a ∈ s`, and `Or.inr b ∈ s.copair t` iff `b ∈ t`.
copair {1, 2} {2, 3} = {inl 1, inl 2, inr 2, inr 3} -/
protected def copair {β} (t₁ : Ordnode α) (t₂ : Ordnode β) : Ordnode (α ⊕ β) :=
merge (map Sum.inl t₁) (map Sum.inr t₂)
