instIsTrichotomousOfIsWellOrder — Mathlib

English

A well-order is trichotomous: for any a,b, either r a b, or r b a, or a = b.

Русский

Хорошо упорядоченное отношение трёхчлено: для любых a,b либо r a b, либо r b a, либо a = b.

LaTeX

$$$\\forall a,b,\\ r\\ a\\ b \\lor r\\ b\\ a \\lor a=b$$$

Lean4

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

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