node3R — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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