rec_pos — Mathlib

English

For nonzero o, CNF(b, o) is the nonempty list representing the Cantor normal form.

Русский

Для ненулевого o CNF(b, o) задает ненулый список Кантора нормальной формы.

LaTeX

$$$\forall b\,\forall o\; (o \neq 0) \Rightarrow CNF(b, o) \neq []$$$

Lean4

theorem rec_pos (b : Ordinal) {o : Ordinal} {C : Ordinal → Sort*} (ho : o ≠ 0) (H0 : C 0)
    (H : ∀ o, o ≠ 0 → C (o % b ^ log b o) → C o) : CNF.rec b H0 H o = H o ho (@CNF.rec b C H0 H _) := by
  rw [CNF.rec, dif_neg]

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