truncate — Mathlib

English

truncate reduces a CofixA F (n+1) tree to CofixA F n by discarding the last level, keeping the same root label.

Русский

truncate переводит дерево CofixA F (n+1) к CofixA F n, отбросив последний уровень, сохранив метку корня.

LaTeX

$$$\operatorname{truncate} : CofixA F (n+1) \to CofixA F n,\quad\operatorname{truncate}(\operatorname{CofixA.intro}\ i\ f) = \operatorname{CofixA.intro}\ i\ (\operatorname{truncate} \circ f).$$$

Lean4

/-- `truncate a` turns `a` into a more limited approximation -/
def truncate : ∀ {n : ℕ}, CofixA F (n + 1) → CofixA F n
  | 0, CofixA.intro _ _ => CofixA.continue
  | succ _, CofixA.intro i f => CofixA.intro i <| truncate ∘ f

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