dual_rotateL — Mathlib

English

The dual of a left rotation equals a right rotation on the duals: dual(rotateL l x r) = rotateR (dual r) x (dual l).

Русский

Дуал левого вращения равен правому вращению на дуалах: dual(rotateL l x r) = rotateR(dual r) x (dual l).

LaTeX

$$$$\operatorname{dual}(\operatorname{rotateL}(l, x, r)) = \operatorname{rotateR}(\operatorname{dual}(r))\, x \, (\operatorname{dual}(l)).$$$$

Lean4

theorem dual_rotateL (l : Ordnode α) (x : α) (r : Ordnode α) : dual (rotateL l x r) = rotateR (dual r) x (dual l) := by
  cases r <;> simp [rotateL, rotateR]; split_ifs <;> simp [dual_node3L, dual_node4L, node3R]

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