equiv_or_fuzzy_zero — Mathlib

English

In an impartial game, either G is equivalent to 0 or G is fuzzy with 0.

Русский

В непредвзятой игре либо G эквивалентна 0, либо G неразрешима с 0.

LaTeX

$$$G \cong 0 \lor G \parallel 0$$$

Lean4

/-- In an impartial game, either the first player always wins, or the second player always wins. -/
theorem equiv_or_fuzzy_zero : G ≈ 0 ∨ G ‖ 0 :=
  by
  rcases lt_or_equiv_or_gt_or_fuzzy G 0 with (h | h | h | h)
  · exact ((nonneg G) h).elim
  · exact Or.inl h
  · exact ((nonpos G) h).elim
  · exact Or.inr h

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