foldr — Mathlib

English

In CNF(b, o), every exponent (the first component of a pair) is ≤ log b o.

Русский

В CNF(b, o) каждый показатель степени (первая компонента пары) не превосходит log b o.

LaTeX

$$$\forall b\,\forall o\, \forall x \in CNF(b, o), x.1 \le \log(b, o)$$$

Lean4

/-- Evaluating the Cantor normal form of an ordinal returns the ordinal. -/
protected theorem foldr (b o : Ordinal) : (CNF b o).foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 = o :=
  by
  refine CNF.rec b ?_ ?_ o
  · rw [zero_right, foldr_nil]
  · intro o ho IH
    rw [CNF.ne_zero ho, foldr_cons, IH, div_add_mod]

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