From 0474a3159138c5cfeba41cabc901c7a6ca3bdb10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 12 Apr 2024 10:59:10 +0200 Subject: [PATCH] doc: suggestion regarding Artinian Co-authored-by: David Thrane Christiansen --- src/Init/WF.lean | 1 + 1 file changed, 1 insertion(+) 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