diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 4b2e1b5618ba..84c5f2c69c7c 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -48,6 +48,7 @@ If a relation is `WellFounded`, it does not allow for an infinite descent along
 
 If the arguments of the recursive calls in a function definition decrease according to
 a well founded relation, then the function terminates.
+Well-founded relations are sometimes called _Artinian_ or said to satisfy the “descending chain condition”.
 -/
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
   | intro (h : ∀ a, Acc r a) : WellFounded r