lt_or_equiv_or_gt_or_fuzzy — Mathlib

English

For any x,y, either x < y, or x ≈ y, or y < x, or x ‖ y.

Русский

Для любых x,y либо x < y, либо x ≈ y, либо y < x, либо x ‖ y.

LaTeX

$$$x < y \lor (x \approx y) \lor y < x \lor (x \|\| y)$$$

Lean4

/-- Exactly one of the following is true (although we don't prove this here). -/
theorem lt_or_equiv_or_gt_or_fuzzy (x y : PGame) : x < y ∨ (x ≈ y) ∨ y < x ∨ x ‖ y :=
  by
  rcases le_or_gf x y with h₁ | h₁ <;> rcases le_or_gf y x with h₂ | h₂
  · right
    left
    exact ⟨h₁, h₂⟩
  · left
    exact ⟨h₁, h₂⟩
  · right
    right
    left
    exact ⟨h₂, h₁⟩
  · right
    right
    right
    exact ⟨h₂, h₁⟩

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