trichotomous — Mathlib

English

If r is a trichotomous relation on α, then for any a,b, either a ≺ b, or a = b, or b ≺ a.

Русский

Если r является тричотомичным отношением на α, то для любых a,b: либо a ≺ b, либо a = b, либо b ≺ a.

LaTeX

$$$\forall a,b : \alpha, a \prec b \lor a = b \lor b \prec a$$$

Lean4

theorem trichotomous [IsTrichotomous α r] : ∀ a b : α, a ≺ b ∨ a = b ∨ b ≺ a :=
  IsTrichotomous.trichotomous

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