instIsStrictTotalOrderOfIsWellOrder

English

A well-order is a strict total order: any two elements are comparable, and the relation is strict and transitive.

Русский

Хорошо упорядоченное отношение представляет собой строгий полный порядок: любые два элемента сравнимы и отношение строгое и транзитивное.

LaTeX

$$$[IsWellOrder\\ α\\ r] \\rightarrow IsStrictTotalOrder α r$$$

Lean4

instance (priority := 100) {α} (r : α → α → Prop) [IsWellOrder α r] : IsStrictTotalOrder α r where
  -- see Note [lower instance priority]

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