编辑“︁Lean Acc关系”︁（章节）

== 介绍 ==

在数学和计算机科学中，许多递归定义需要满足'''良基性'''（Well-foundedness）才能保证其合法性。Acc关系正是Lean中表示良基关系的一种方式。具体来说，给定一个二元关系`r : α → α → Prop`，若`x : α`满足`Acc r x`，则表示从`x`出发不存在无限下降链`x ≻ x₁ ≻ x₂ ≻ ...`（其中`≻`表示关系`r`）。

换句话说，`Acc r x`断言“`x`在关系`r`下是可访问的”，即所有从`x`开始的`r`-递减序列必然终止。这一性质是定义递归函数或进行归纳证明时的关键工具。