identical_zero_iff — Mathlib

English

An equivalence to 0 holds exactly when both left and right move sets are empty.

Русский

Эквивалентность нулю держится ровно тогда, когда оба множества ходов слева и справа пусты.

LaTeX

$$$ x \equiv 0 \iff \bigl( LeftMoves(x) = \emptyset \bigr) \land \bigl( RightMoves(x) = \emptyset \bigr) $$$

Lean4

theorem identical_zero_iff : ∀ (x : PGame), x ≡ 0 ↔ IsEmpty x.LeftMoves ∧ IsEmpty x.RightMoves
  | mk xl xr xL xR => by
    constructor
    · rintro ⟨h₁, h₂⟩
      dsimp [Relator.BiTotal, Relator.LeftTotal, Relator.RightTotal] at h₁ h₂
      simp_rw [IsEmpty.forall_iff, and_true, IsEmpty.exists_iff] at h₁ h₂
      exact ⟨⟨h₁⟩, ⟨h₂⟩⟩
    · rintro ⟨h₁, h₂⟩
      exact identical_of_isEmpty _ _

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