congr_left — Mathlib

English

If two PGames have the same left and right move relations to all other games, then they are identical.

Русский

Если две PGame имеют одинаковые отношения левых и правых ходов к каждому другому игре, то они идентичны.

LaTeX

$$$ \\forall {x y : PGame}, (\\forall z, z.mem_\\ell x \\leftrightarrow z.mem_\\ell y) \\land (\\forall z, z.mem_\\mathrm{r} x \\leftrightarrow z.mem_\\mathrm{r} y) \\rightarrow x \\equiv y$$

Lean4

theorem congr_left : ∀ {x y : PGame}, x ≡ y → (∀ {w : PGame}, x ∈ᵣ w ↔ y ∈ᵣ w)
  | _, _, h, mk _ _ _ _ => ⟨fun ⟨i, hi⟩ ↦ ⟨i, h.symm.trans hi⟩, fun ⟨i, hi⟩ ↦ ⟨i, h.trans hi⟩⟩

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