node3L — Mathlib

English

The size of node3L is the sum of the sizes of its subtrees plus 2 for the node itself.

Русский

Размер node3L равен сумме размеров поддеревьев плюс 2 за сам узел.

LaTeX

$$$$\operatorname{size}(\operatorname{node3L}(l, x, m, y, r)) = \operatorname{size}(l) + \operatorname{size}(m) + \operatorname{size}(r) + 2.$$$$

Lean4

theorem node3L {l x m y r} (hl : @Sized α l) (hm : Sized m) (hr : Sized r) : Sized (node3L l x m y r) :=
  (hl.node' hm).node' hr

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