isTrichotomous — Mathlib

English

If r is total, then it is trichotomous: for any a,b, either r(a,b) or r(b,a).

Русский

Если r суммарно, то выполняется тричотомия: для любых a,b либо r(a,b), либо r(b,a).

LaTeX

$$$\\\\forall a,b, \\\\ r(a,b) \\\\lor \\\\ r(b,a).$$$

Lean4

protected theorem isTrichotomous (r) [IsTotal α r] : IsTrichotomous α r :=
  ⟨fun a b => or_left_comm.1 (Or.inr <| total_of r a b)⟩
    -- see Note [lower instance priority]

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