English
A strict order r is well-founded if and only if there is no infinite descending chain with respect to r; equivalently, there is no embedding of (ℕ, >) into r.
Русский
Строгий порядок r хорошо основан тогда и только тогда, когда не существует бесконечной нисходящей цепи по отношению к r; эквивалентно отсутствию вложения от (ℕ, >) в r.
LaTeX
$$$$\mathrm{WellFounded}(r) \iff \mathrm{IsEmpty}\big(((\cdot > \cdot) : \mathbb{N} \to \mathbb{N} \to \mathrm{Prop}) \hookrightarrow_r r\big).$$$$
Lean4
/-- A strict order relation is well-founded iff it doesn't have any infinite descending chain.
See `wellFounded_iff_isEmpty_descending_chain` for a version which works on any relation. -/
theorem wellFounded_iff_isEmpty : WellFounded r ↔ IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r)
where
mp := fun ⟨h⟩ ↦ ⟨fun f ↦ f.not_acc 0 (h _)⟩
mpr _ := ⟨fun _x ↦ acc_iff_isEmpty_subtype_mem_range.2 inferInstance⟩
