English
The negation of a game built from lists L and R equals the game built from negated lists, with the lists swapped.
Русский
Отрицание игры, заданной списками L и R, равно игре, построенной из отрицаний элементов R и L соответственно, с обменом частей.
LaTeX
$$$$ -\mathrm{ofLists}(L,R) = \mathrm{ofLists}(\mathrm{map}( -\cdot ) R, \mathrm{map}( -\cdot ) L). $$$$
Lean4
@[simp]
theorem neg_ofLists (L R : List PGame) : -ofLists L R = ofLists (R.map fun x => -x) (L.map fun x => -x) :=
by
simp only [ofLists, neg_def, List.getElem_map, mk.injEq, List.length_map, true_and]
constructor
all_goals
apply hfunext
· simp
· rintro ⟨⟨a, ha⟩⟩ ⟨⟨b, hb⟩⟩ h
have : ∀ {m n} (_ : m = n) {b : ULift (Fin m)} {c : ULift (Fin n)} (_ : b ≍ c), (b.down : ℕ) = ↑c.down :=
by
rintro m n rfl b c
simp only [heq_eq_eq]
rintro rfl
rfl
simp only [heq_eq_eq]
congr 5
exact this (List.length_map _).symm h
