dual_node3R — Mathlib

English

The dual of a node3R structure is node3L on the duals of its subparts with swapped positions.

Русский

Дуал узла3R даёт узел3L на дуалах его поддеревьев с поменянными местами левой и правой стороны.

LaTeX

$$$$\operatorname{dual}(\operatorname{node3R}(l, x, m, y, r)) = \operatorname{node3L}(\operatorname{dual}(r), y, \operatorname{dual}(m), x, \operatorname{dual}(l)).$$$$

Lean4

theorem dual_node3R (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
    dual (node3R l x m y r) = node3L (dual r) y (dual m) x (dual l) := by simp [node3L, node3R, add_comm]

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