balance' — Mathlib

English

If l and r are sized, then balance'(l, x, r) is sized.

Русский

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

LaTeX

$$(Sized(l)) ∧ (Sized(r)) ⟶ Sized(\mathrm{balance'}(l, x, r))$$

Lean4

theorem balance' {l x r} (hl : @Sized α l) (hr : Sized r) : Sized (balance' l x r) :=
  by
  unfold Ordnode.balance'; split_ifs
  · exact hl.node' hr
  · exact hl.rotateL hr
  · exact hl.rotateR hr
  · exact hl.node' hr

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