English
Let r be a strict order on α, and let f be an order-embedding from (ℕ, >) into r. Then for every k ∈ ℕ, the element f(k) is not accessible with respect to r; i.e., there is an infinite descending r-chain starting at f(k).
Русский
Пусть r — строгий порядок на α, и пусть f — вложение порядка из (ℕ, >) в r. Тогда для каждого k ∈ ℕ элемент f(k) не достижим по отношению Acc_r; то есть из f(k) можно продолжать бесконечную нисходящую последовательность по r.
LaTeX
$$$$\forall f:\ ((\cdot > \cdot) : \mathbb{N} \to \mathbb{N} \to \mathrm{Prop}) \hookrightarrow_r r,\ \forall k \in \mathbb{N},\ \neg \mathrm{Acc}_r(f(k)).$$$$
Lean4
theorem not_acc (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) (k : ℕ) : ¬Acc r (f k) :=
by
rw [acc_iff_isEmpty_subtype_mem_range, not_isEmpty_iff]
exact ⟨⟨f, k, rfl⟩⟩
