size_balance' — Mathlib

English

If l and r are sized, then the size of balance'(l, x, r) equals size(l) + size(r) + 1.

Русский

Если поддеревья l и r ограничены по размеру, то размер balance'(l, x, r) равен size(l) + size(r) + 1.

LaTeX

$$\operatorname{Sized}(l) ∧ \operatorname{Sized}(r) ⟶ \operatorname{size}(l.balance'(x, r)) = \operatorname{size}(l) + \operatorname{size}(r) + 1$$

Lean4

theorem size_balance' {l x r} (hl : @Sized α l) (hr : Sized r) : size (@balance' α l x r) = size l + size r + 1 :=
  by
  unfold balance'; split_ifs
  · rfl
  · exact hr.rotateL_size
  · exact hl.rotateR_size
  · rfl

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