birthday_eq_zero — Mathlib

English

For every game x, birthday x = 0 if and only if x = 0.

Русский

Для любой игры x день рождения x равен 0 тогда и только тогда, когда x = 0.

LaTeX

$$$\operatorname{birthday}(x) = 0 \iff x = 0$$$

Lean4

@[simp]
theorem birthday_eq_zero {x : Game} : birthday x = 0 ↔ x = 0 :=
  by
  constructor
  · intro h
    let ⟨y, hy₁, hy₂⟩ := birthday_eq_pGameBirthday x
    rw [← hy₁]
    rw [h, PGame.birthday_eq_zero] at hy₂
    exact PGame.game_eq (@PGame.Equiv.isEmpty _ hy₂.1 hy₂.2)
  · rintro rfl
    exact birthday_zero

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