instWellFoundedRelation_mathlib — Mathlib

English

On Fin n, the relation defined by the natural measure val is well-founded.

Русский

На Fin n отношение, заданное естественной мерой val, является оканчиваемым.

LaTeX

$$Finite-well-founded relation on Fin(n) with measure val$$

Lean4

/-- Use the ordering on `Fin n` for checking recursive definitions.

For example, the following definition is not accepted by the termination checker,
unless we declare the `WellFoundedRelation` instance:
```lean
def factorial {n : ℕ} : Fin n → ℕ
  | ⟨0, _⟩ := 1
  | ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
```
-/
instance {n : ℕ} : WellFoundedRelation (Fin n) :=
  measure (val : Fin n → ℕ)

Похожие утверждения