dual_node4R — Mathlib

English

The dual of a node4R is node4L on the duals of its subparts with swapped sides.

Русский

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

LaTeX

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

Lean4

theorem dual_node4R (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
    dual (node4R l x m y r) = node4L (dual r) y (dual m) x (dual l) := by
  cases m <;> simp [node4L, node4R, node3L, dual_node3R, add_comm]

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