impartial_congr — Mathlib

English

Relabelling preserves impartiality: if G ≡r H and G is impartial, then H is impartial.

Русский

Перекодирование сохраняет непредвзятость: если G ≡r H и G непредвзята, то H непредвзята.

LaTeX

$$$(G \equiv_r H) \Rightarrow (\operatorname{Impartial}(G) \Rightarrow \operatorname{Impartial}(H))$$$

Lean4

theorem impartial_congr {G H : PGame} (e : G ≡r H) [G.Impartial] : H.Impartial :=
  impartial_def.2
    ⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)), fun i =>
      impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
termination_by G

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