lt_or_eq_or_gt_or_incompRel — Mathlib

English

For any a,b in a partially ordered set, exactly one of a<b, a=b, b<a, or a and b are incomparable holds.

Русский

Для любых a, b в частично упорядоченном множестве верно: либо a<b, либо a=b, либо b<a, либо a и b несопоставимы.

LaTeX

$$$a < b \,\\lor \, a = b \,\\lor \, b < a \,\\lor \, IncompRel(\\le) a b$$$

Lean4

/-- Exactly one of the following is true. -/
theorem lt_or_eq_or_gt_or_incompRel [PartialOrder α] (a b : α) : a < b ∨ a = b ∨ b < a ∨ IncompRel (· ≤ ·) a b := by
  simpa using lt_or_antisymmRel_or_gt_or_incompRel a b

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