English
Under a strongly atomic setting with a natural-grade order, there exists an order-embedding of N into α starting at the bottom, with finite covariances between consecutive elements.
Русский
Для строго атомарной структуры с натуральным порядком существует биекция-запись: есть вложение порядка из натуральных чисел в α, начинающееся с нуля, такое что последовательные элементы образуют каскады кофакторов.
LaTeX
$$$\\exists f: \\mathbb{N} \\hookrightarrow o \\alpha, f(0)=\\bot, \\forall i, f(i) \\ll f(i+1).$$$
Lean4
theorem exists_nat_orderEmbedding_of_forall_covby_finite [GradeMinOrder ℕ α] [OrderBot α] [Infinite α]
(hfin : ∀ (a : α), {x | a ⋖ x}.Finite) : ∃ f : ℕ ↪o α, f 0 = ⊥ ∧ (∀ i, f i ⋖ f (i + 1)) ∧ ∀ i, grade ℕ (f i) = i :=
by
obtain ⟨f, h0, hf⟩ := exists_orderEmbedding_covby_of_forall_covby_finite_of_bot hfin
refine ⟨f, h0, hf, fun i ↦ ?_⟩
induction i with
| zero => simp [h0]
| succ i ih => simpa [Order.covBy_iff_add_one_eq, ih, eq_comm] using CovBy.grade ℕ <| hf i
