lf_or_equiv_or_gf — Mathlib

English

For any x, y in PGame, either x ⧏ y, or x ≈ y, or y ⧏ x.

Русский

Для любых x, y из PGame верно: либо x ⧏ y, или x ≈ y, или y ⧏ x.

LaTeX

$$$\forall x,y \in \mathrm{PGame},\ x \mathrel{⧏} y \lor (x \approx y) \lor y \mathrel{⧏} x$$$

Lean4

theorem lf_or_equiv_or_gf (x y : PGame) : x ⧏ y ∨ (x ≈ y) ∨ y ⧏ x :=
  by
  rw [or_iff_not_imp_left]
  intro h
  rcases lt_or_equiv_of_le (PGame.not_lf.1 h) with h' | h'
  · exact Or.inr h'.lf
  · exact Or.inl (Equiv.symm h')

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