English
O(m * n). The Cartesian product of two sets represented as trees: t1 and t2. The product contains all pairs (a,b) with a ∈ t1 and b ∈ t2.
Русский
O(m * n). Декартово произведение двух множеств, представленных деревьями t1 и t2. Содержит все пары (a,b), где a∈t1 и b∈t2.
LaTeX
$$$$ \mathrm{prod}: (t_1 : Ordnode\; \alpha) \to (t_2 : Ordnode\; \beta) \to Ordnode\; (\alpha \times \beta), \quad \mathrm{prod}(t_1,t_2) = \text{пополнение дерева пар} $$$$
Lean4
/-- O(m * n). The Cartesian product of two sets: `(a, b) ∈ s.prod t` iff `a ∈ s` and `b ∈ t`.
prod {1, 2} {2, 3} = {(1, 2), (1, 3), (2, 2), (2, 3)} -/
protected def prod {β} (t₁ : Ordnode α) (t₂ : Ordnode β) : Ordnode (α × β) :=
fold nil (fun s₁ a s₂ => merge s₁ <| merge (map (Prod.mk a) t₂) s₂) t₁
