Theorems · Theorem · order theory
wellFounded_iff_isEmpty_descending_chain
∀ {α : Sort u_1} {r : α → α → Prop}, WellFounded r ↔ IsEmpty { f // ∀ (n : ℕ), r (f (n + 1)) (f n) }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.
- Defined in
- Mathlib.Order.WellFounded
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsEmptystatement and proof · cited by 759
- IsEmpty.falseproof · cited by 24
- acc_iff_isEmpty_descending_chainproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- SSet.Subcomplex.PairingCore.isRegular_pairing_iffproof · cited by 4
- SSet.Subcomplex.Pairing.WeakRankFunction.wf_ancestralRelproof · cited by 1
- SSet.Subcomplex.Pairing.RankFunction.wf_ancestralRelproof · cited by 1
- SetRel.IsWellFounded.inv_of_finiteDimensionalproof · cited by 1
- WellFounded.not_rel_apply_succproof · cited by 0