impartial_neg — Mathlib

English

If G is impartial, then its negation −G is impartial.

Русский

Если G непредвзята, то её отрицание −G непредвзято.

LaTeX

$$$\operatorname{Impartial}(G) \Rightarrow \operatorname{Impartial}(-G)$$$

Lean4

instance impartial_neg (G : PGame) [G.Impartial] : (-G).Impartial :=
  by
  rw [impartial_def]
  refine ⟨?_, fun i => ?_, fun i => ?_⟩
  · rw [neg_neg]
    exact Equiv.symm (neg_equiv_self G)
  · rw [moveLeft_neg]
    exact impartial_neg _
  · rw [moveRight_neg]
    exact impartial_neg _
termination_by G

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