lt_or_antisymmRel_or_gt_or_incompRel

English

Exactly one of the following holds for a,b: a < b, or AntisymmRel r a b, or b < a, or IncompRel r a b.

Русский

Для любых a,b верно одно из: a < b, или AntisymmRel r a b, или b < a, или IncompRel r a b.

LaTeX

$$a < b \lor AntisymmRel(≤) a b \lor b < a \lor IncompRel(≤) a b$$

Lean4

/-- Exactly one of the following is true. -/
theorem lt_or_antisymmRel_or_gt_or_incompRel (a b : α) :
    a < b ∨ AntisymmRel (· ≤ ·) a b ∨ b < a ∨ IncompRel (· ≤ ·) a b :=
  by
  simp_rw [lt_iff_le_not_ge]
  tauto

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