English
Characterization of right-move membership in a sum: x ∈ᵣ y₁ + y₂ iff there exists z ∈ᵣ y₁ with x ≡ z + y₂, or there exists z ∈ᵣ y₂ with x ≡ y₁ + z.
Русский
Характеризация принадлежности правому ходу в сумме: x ∈ᵣ y₁ + y₂ тогда и только тогда, когда существует z ∈ᵣ y₁ такое, что x ≡ z + y₂, или существует z ∈ᵣ y₂ такое, что x ≡ y₁ + z.
LaTeX
$$$ x \in^\!r (y_1+y_2) \iff (\exists z \in^\!r y_1, x \equiv z + y_2) \lor (\exists z \in^\!r y_2, x \equiv y_1 + z) $$$
Lean4
theorem memᵣ_add_iff {x y₁ y₂ : PGame} : x ∈ᵣ y₁ + y₂ ↔ (∃ z ∈ᵣ y₁, x ≡ z + y₂) ∨ (∃ z ∈ᵣ y₂, x ≡ y₁ + z) :=
by
obtain ⟨y₁l, y₁r, y₁L, y₁R⟩ := y₁
obtain ⟨y₂l, y₂r, y₂L, y₂R⟩ := y₂
constructor
· rintro ⟨(i | i), hi⟩
exacts [.inl ⟨y₁R i, moveRight_memᵣ _ _, hi⟩, .inr ⟨y₂R i, moveRight_memᵣ _ _, hi⟩]
· rintro (⟨_, ⟨i, hi⟩, h⟩ | ⟨_, ⟨i, hi⟩, h⟩)
exacts [⟨.inl i, h.trans hi.add_right⟩, ⟨.inr i, h.trans hi.add_left⟩]
