dual_node4L — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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