English
In the Cantor normal form CNF(b, o), the exponents (the first components of the pairs) form a strictly decreasing sequence with respect to the order >.
Русский
Показатели в канторовой нормальной форме CNF(b, o) образуют строго убывающий порядок: последовательность первых компонентов пар убывает по отношению к >.
LaTeX
$$$$ ((CNF(b,o)).map \\text{fst}).Sorted(\\, > \\,) $$$$
Lean4
/-- The exponents of the Cantor normal form are decreasing. -/
protected theorem sorted (b o : Ordinal) : ((CNF b o).map Prod.fst).Sorted (· > ·) :=
by
refine CNF.rec b ?_ (fun o ho IH ↦ ?_) o
· rw [zero_right]
exact sorted_nil
· rcases le_or_gt b 1 with hb | hb
· rw [CNF.of_le_one hb ho]
exact sorted_singleton _
· obtain hob | hbo := lt_or_ge o b
· rw [CNF.of_lt ho hob]
exact sorted_singleton _
· rw [CNF.ne_zero ho, map_cons, sorted_cons]
refine ⟨fun a H ↦ ?_, IH⟩
rw [mem_map] at H
rcases H with ⟨⟨a, a'⟩, H, rfl⟩
exact (fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb hbo)
