identical_of_isEmpty — Mathlib

English

If two PGames have empty left and right moves, they are identical.

Русский

Если у двух PGame пустые левые и правые ходы, они идентичны.

LaTeX

$$$ \forall x,y : PGame,\ IsEmpty x.LeftMoves \land IsEmpty x.RightMoves \land IsEmpty y.LeftMoves \land IsEmpty y.RightMoves \Rightarrow x \equiv y $$$

Lean4

theorem identical_of_isEmpty (x y : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] [IsEmpty y.LeftMoves]
    [IsEmpty y.RightMoves] : x ≡ y :=
  identical_iff.2 (by simp [biTotal_empty])

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