toPGame_equiv_iff — Mathlib

English

Two ordinals a and b have equivalent P-games, a.toPGame ≈ b.toPGame, if and only if a = b.

Русский

Два ординала a и b имеют эквивалентные P-игры, если и только если a = b.

LaTeX

$$(a.toPGame ≈ b.toPGame) \iff a = b$$

Lean4

@[simp]
theorem toPGame_equiv_iff {a b : Ordinal} : (a.toPGame ≈ b.toPGame) ↔ a = b := by
  -- Porting note: was `rw [PGame.Equiv]`

  change _ ≤ _ ∧ _ ≤ _ ↔ _
  rw [le_antisymm_iff, toPGame_le_iff, toPGame_le_iff]

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