English
Let x and y be ply games. If for every left move of x there exists a left move of y whose resulting positions are equivalent, and for every right move of x there exists a right move of y whose resulting positions are equivalent, and conversely for moves from y to x, then x is equivalent to y.
Русский
Пусть x и y — игры PGame. Если для каждого левого хода x существует соответствующий левый ход y, дающий эквивалентное положение, и для каждого правого хода x существует соответствующий правый ход y с эквивалентным положением, и наоборот для ходов из y в x, то x эквивалентно y.
LaTeX
$$$\Big(\forall i, \exists j\, x.moveLeft i \approx y.moveLeft j\Big) \land \Big(\forall i, \exists j\, x.moveRight i \approx y.moveRight j\Big) \land \Big(\forall j, \exists i\, x.moveLeft i \approx y.moveLeft j\Big) \land \Big(\forall j, \exists i\, x.moveRight i \approx y.moveRight j\Big) \Rightarrow x \approx y$$$
Lean4
theorem of_exists {x y : PGame} (hl₁ : ∀ i, ∃ j, x.moveLeft i ≈ y.moveLeft j)
(hr₁ : ∀ i, ∃ j, x.moveRight i ≈ y.moveRight j) (hl₂ : ∀ j, ∃ i, x.moveLeft i ≈ y.moveLeft j)
(hr₂ : ∀ j, ∃ i, x.moveRight i ≈ y.moveRight j) : x ≈ y :=
by
constructor <;> refine le_def.2 ⟨?_, ?_⟩ <;> intro i
· obtain ⟨j, hj⟩ := hl₁ i
exact Or.inl ⟨j, Equiv.le hj⟩
· obtain ⟨j, hj⟩ := hr₂ i
exact Or.inr ⟨j, Equiv.le hj⟩
· obtain ⟨j, hj⟩ := hl₂ i
exact Or.inl ⟨j, Equiv.ge hj⟩
· obtain ⟨j, hj⟩ := hr₁ i
exact Or.inr ⟨j, Equiv.ge hj⟩
