English
An element x is Acc r if and only if there is no infinite decreasing r-chain with x appearing in the range of such a chain embedding.
Русский
Элемент x является Acc r тогда и только тогда, когда не существует бесконечной нисходящей по r последовательности, начинающейся из x и служащей образом в диапазоне вложения.
LaTeX
$$$ Acc(r,x) \\iff IsEmpty\\left(\\{ f : ((\\cdot > \\cdot) : \\mathbb{N} \\to \\mathbb{N} \\to \\mathrm{Prop}) \\hookrightarrow_r r \\;\\big|\\; x \\in \\mathrm{range}\\, f \\}\\right) $$
Lean4
/-- A value is accessible iff it isn't contained in any infinite decreasing sequence. -/
theorem acc_iff_isEmpty_subtype_mem_range {x} :
Acc r x ↔ IsEmpty { f : ((· > ·) : ℕ → ℕ → Prop) ↪r r // x ∈ Set.range f }
where
mp
acc :=
.mk fun ⟨f, k, hk⟩ ↦
not_acc_iff_exists_descending_chain.mpr ⟨(f <| k + ·), hk, fun _n ↦ f.map_rel_iff.2 (Nat.lt_succ_self _)⟩ acc
mpr
h :=
of_not_not fun nacc ↦
have ⟨f, hf⟩ := not_acc_iff_exists_descending_chain.mp nacc
h.elim ⟨natGT f hf.2, 0, hf.1⟩
