node3L_size — Mathlib

English

The same size formula for node3L as before: size(l) + size(m) + size(r) + 2.

Русский

Та же формула размера для node3L: размер(l) + размер(m) + размер(r) + 2.

LaTeX

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

Lean4

theorem node3L_size {l x m y r} : size (@node3L α l x m y r) = size l + size m + size r + 2 := by
  dsimp [node3L, node', size]; rw [add_right_comm _ 1]

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