ext — Mathlib

English

If two PGames have identical left and right move relations to every game, 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 ext : ∀ {x y}, (∀ z, z ∈ₗ x ↔ z ∈ₗ y) → (∀ z, z ∈ᵣ x ↔ z ∈ᵣ y) → x ≡ y
  | mk _ _ _ _, mk _ _ _ _, hl, hr =>
    identical_iff'.mpr
      ⟨⟨fun i ↦ (hl _).mp ⟨i, refl _⟩, fun j ↦ (hl _).mpr ⟨j, refl _⟩⟩,
        ⟨fun i ↦ (hr _).mp ⟨i, refl _⟩, fun j ↦ (hr _).mpr ⟨j, refl _⟩⟩⟩

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