English
A relation is well-founded if and only if there is no infinite descending chain; equivalently the set of descending chains is empty.
Русский
Отношение хорошо основано тогда и только тогда, когда не существует бесконечной нисходящей цепи; эквивалентно тому, что множество нисходящих цепей пусто.
LaTeX
$$$WellFounded r \iff IsEmpty { f : \mathbb{N} \to α \mid \forall n, r (f(n+1)) (f n) }$$$
Lean4
/-- A relation is well-founded iff it doesn't have any infinite descending chain.
See `RelEmbedding.wellFounded_iff_isEmpty` for a version in terms of relation embeddings. -/
theorem wellFounded_iff_isEmpty_descending_chain {α} {r : α → α → Prop} :
WellFounded r ↔ IsEmpty { f : ℕ → α // ∀ n, r (f (n + 1)) (f n) }
where
mp := fun ⟨h⟩ ↦ ⟨fun ⟨f, hf⟩ ↦ (acc_iff_isEmpty_descending_chain.mp (h (f 0))).false ⟨f, rfl, hf⟩⟩
mpr h := ⟨fun _ ↦ acc_iff_isEmpty_descending_chain.mpr ⟨fun ⟨f, hf⟩ ↦ h.false ⟨f, hf.2⟩⟩⟩
