instWellFoundedRelationLexOfWellFoundedLT

English

There exists a well-founded relation on Lex(α × β) defined by the lexicographic order, provided α and β have well-founded lt relations.

Русский

Существует хорошо основанное отношение на Lex(α × β), заданное лексикографическим порядком, если на α и β заданы хорошо основанные отношения меньшего.

LaTeX

$$$$ \text{WellFoundedRelation}(<_{\mathrm{lex}}) \text{ on } \mathrm{Lex}(\alpha \times \beta) $$$$

Lean4

instance [LT α] [LT β] [WellFoundedLT α] [WellFoundedLT β] : WellFoundedRelation (α ×ₗ β) :=
  ⟨(· < ·), wellFounded_lt⟩

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