rotateR_size — Mathlib

English

If l is sized, size(rotateR(l, x, r)) = size(l) + size(r) + 1.

Русский

Пусть l ограничено по размеру; тогда размер rotateR(l, x, r) равен size(l) + size(r) + 1.

LaTeX

$$\operatorname{Sized}(l) \Rightarrow \operatorname{size}(\mathrm{rotateR}(l, x, r)) = \operatorname{size}(l) + \operatorname{size}(r) + 1$$

Lean4

theorem rotateR_size {l x r} (hl : Sized l) : size (@Ordnode.rotateR α l x r) = size l + size r + 1 := by
  rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]

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