eq_node' — Mathlib

English

If a node is Sized, then it equals its canonical representation node' on its left/right subparts.

Русский

Если узел имеет размер, то он равен своей канонической записи node' на левой и правой частях.

LaTeX

$$$\\forall s\\ l\\ x\\ r,\\ h : Sized(\\mathrm{node}\\ s\\ l\\ x\\ r)\\Rightarrow \\mathrm{node}\\ s\\ l\\ x\\ r = .\\mathrm{node'}\\ l\\ x\\ r$$$

Lean4

theorem eq_node' {s l x r} (h : @Sized α (node s l x r)) : node s l x r = .node' l x r := by rw [h.1]

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