instIsWellFoundedChainsLex_chains

English

If α with relation r is well-founded, then the instance giving IsWellFounded for List.chains r via List.lex_chains r holds.

Русский

Если множество с отношением r хорошо основано, то существует экземпляр, который сообщает о хорошо основанности списков цепей через лексическое упорядочение.

LaTeX

$$$[IsWellFounded\\ α\\ r]\\Rightarrow IsWellFounded\\ (List.chains\\ r)\\ (List.lex\\_chains\\ r)$$$

Lean4

instance [hwf : IsWellFounded α r] : IsWellFounded (List.chains r) (List.lex_chains r) :=
  ⟨hwf.wf.list_chain'⟩

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