English
CNF.rec_pos provides the explicit evaluation for CNF by unfolding the recursive definition at a nonzero base.
Русский
CNF.rec_pos задает явное вычисление CNF через распаковку рекурсивного определения для ненулевого основания.
LaTeX
$$$\forall b\, \forall o\; (ho : o \neq 0) \; \forall C:\ Ordinal \to \text{Sort}^* ,\; CNF.rec(b, H0, H)(o) = H(o, ho, CNF.rec(b, H0, H)(\text{прочее}))$$$
Lean4
/-- Every exponent in the Cantor normal form `CNF b o` is less or equal to `log b o`. -/
theorem fst_le_log {b o : Ordinal.{u}} {x : Ordinal × Ordinal} : x ∈ CNF b o → x.1 ≤ log b o :=
by
refine CNF.rec b ?_ (fun o ho H ↦ ?_) o
· simp
· rw [CNF.ne_zero ho, mem_cons]
rintro (rfl | h)
· rfl
· exact (H h).trans (log_mono_right _ (mod_opow_log_lt_self b ho).le)
