dual_balanceR — Mathlib

English

The dual of balanceR equals balanceL on the duals: dual (balanceR l x r) = balanceL (dual r) x (dual l).

Русский

Дуал balanceR равен balanceL на дуалах: dual(balanceR(l,x,r)) = balanceL(dual(r)) x (dual(l)).

LaTeX

$$$$\operatorname{dual}(\operatorname{balanceR}(l, x, r)) = \operatorname{balanceL}(\operatorname{dual}(r)) \ x \ (\operatorname{dual}(l)).$$$$

Lean4

theorem dual_balanceR (l : Ordnode α) (x : α) (r : Ordnode α) : dual (balanceR l x r) = balanceL (dual r) x (dual l) :=
  by rw [← dual_dual (balanceL _ _ _), dual_balanceL, dual_dual, dual_dual]

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