English
Let A and B be finite sets of trees with unit leaves. The pairwiseNode(A,B) consists of all trees formed by taking a left subtree from A and a right subtree from B using the binary operation △.
Русский
Пусть A и B — конечные множества деревьев с листами типа Unit. pairwiseNode(A,B) состоит из всех деревьев, полученных соединением левого поддерева из A и правого из B с помощью операции △.
LaTeX
$$$\\mathrm{pairwiseNode}(A,B) = \\{\\, t_1 \\triangle t_2 \\mid t_1 \\in A,\\ t_2 \\in B \\,\\}$$$
Lean4
/-- Given two finsets, find all trees that can be formed with
left child in `a` and right child in `b` -/
abbrev pairwiseNode (a b : Finset (Tree Unit)) : Finset (Tree Unit) :=
(a ×ˢ b).map ⟨fun x => x.1 △ x.2, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => fun h => by simpa using h⟩
