English
If a relation r is well-founded, then the lexicographic order on r-decreasing chains is well-founded.
Русский
Если отношение r хорошо основано, то лексикографический порядок на цепях, уменьшающихся по r, тоже хорошо основан.
LaTeX
$$$WellFounded\\ r\\Rightarrow WellFounded\\ (List.lex\\_chains\\ r)$$$
Lean4
/-- If an `r`-decreasing chain `l` is empty or its head is accessible by `r`, then
`l` is accessible by the lexicographic order `List.Lex r`. -/
theorem list_chain' {l : List.chains r} (acc : ∀ a ∈ l.val.head?, Acc r a) : Acc (List.lex_chains r) l :=
by
obtain ⟨_ | ⟨a, l⟩, hl⟩ := l
· apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
specialize acc a _
·
rw [List.head?_cons, Option.mem_some_iff]
/- For an r-decreasing chain of the form a :: l, apply induction on a -/
induction acc generalizing l with
| intro a _ ih =>
/- Bundle l with a proof that it is r-decreasing to form l' -/
have hl' := (List.isChain_cons'.1 hl).2
let l' : List.chains r := ⟨l, hl'⟩
have : Acc (List.lex_chains r) l' := by
rcases l with - | ⟨b, l⟩
· apply Acc.intro;
rintro ⟨_⟩
⟨_⟩
/- l' is accessible by induction hypothesis -/
·
apply
ih b
(List.isChain_cons_cons.1 hl).1
/- make l' a free variable and induct on l' -/
revert hl
rw [(by rfl : l = l'.1)]
clear_value l'
induction this with
| intro l _ ihl =>
intro hl
apply Acc.intro
rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
· apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
· apply ih b hr
· apply ihl ⟨m, (List.isChain_cons'.1 hm).2⟩ hr
