dual_rotateR — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem dual_rotateR (l : Ordnode α) (x : α) (r : Ordnode α) : dual (rotateR l x r) = rotateL (dual r) x (dual l) := by
  rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]

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