node3R_size — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem node3R_size {l x m y r} : size (@node3R α l x m y r) = size l + size m + size r + 2 := by
  dsimp [node3R, node', size]; rw [← add_assoc, ← add_assoc]

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