ne_zero — Mathlib

English

Equivalently, CNF.ne_zero gives the canonical recursive decomposition of a nonzero ordinal into its CNF head and tail.

Русский

CNF.ne_zero задает разложение ненулевого ординала на голову и хвост канторовской нормальной формы.

LaTeX

$$$\forall b\,\forall o\; (o \neq 0) \Rightarrow CNF(b, o) = (\log_b(o),\, o / b^{\log_b(o)}) :: CNF(b, o \% b^{\log_b(o)})$$$

Lean4

/-- Recursive definition for the Cantor normal form. -/
protected theorem ne_zero {b o : Ordinal} (ho : o ≠ 0) :
    CNF b o = (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) :=
  rec_pos b ho _ _

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