instIsWellFounded — Mathlib

English

If α and β are well-founded with r and s, then the lexicographic order on α × β is well-founded.

Русский

Если α и β хорошо основаны по r и s, то лексикографическое упорядочение на α × β хорошо основано.

LaTeX

$$$[IsWellFounded α r] [IsWellFounded β s] : IsWellFounded (Prod α β) (Prod.Lex r s)$$$

Lean4

instance instIsWellFounded [IsWellFounded α r] [IsWellFounded β s] : IsWellFounded (α × β) (Prod.Lex r s) :=
  ⟨IsWellFounded.wf.prod_lex IsWellFounded.wf⟩

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