list_chain' — Mathlib

English

If a relation is well-founded, then the collection of chains with the lexicographic ordering is well-founded.

Русский

Если отношение хорошо основано, то множество цепей с лексикографическим порядком хорошо основано.

LaTeX

$$$\\text{WellFounded }\\ r\\Rightarrow \\text{WellFounded }\\ (List.chains\\ r, List.lex\\_chains\\ r)$$$

Lean4

/-- If `r` is well-founded, the lexicographic order on `r`-decreasing chains is also. -/
theorem list_chain' (hwf : WellFounded r) : WellFounded (List.lex_chains r) :=
  ⟨fun _ ↦ Acc.list_chain' (fun _ _ => hwf.apply _)⟩

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