dual_node' — Mathlib

English

The dual of the tilted node with left and right subtrees is the node formed by swapping the duals of the subtrees and keeping the middle element fixed.

Русский

Дуал повернутого узла с левым и правым поддеревьями получается узлом, в котором местами поменяны дуалы поддеревьев, а средний элемент остается неизменным.

LaTeX

$$$\\mathrm{dual}(\\mathrm{node}'\\ l\\ x\\ r) = \\mathrm{node}'(\\mathrm{dual}(r))\\ x\\ (\\mathrm{dual}(l))$$$

Lean4

theorem dual_node' (l : Ordnode α) (x : α) (r : Ordnode α) : dual (node' l x r) = node' (dual r) x (dual l) := by
  simp [node', add_comm]

Похожие утверждения