birthday_eq_pGameBirthday

Mathlib.SetTheory.Game.Birthday

URI: https://scilib.ai/kg/mathlib#SetTheory.Game.birthday_eq_pGameBirthday

← MathLib Explorer

English

There exists y in PGame such that y ≈ x and y.birthday = birthday x.

Русский

Существует y в PGame такое, что y эквивалентно x и y.birthday = birthday x.

LaTeX

$$$ \exists y : PGame, y \approx x \land y.birthday = birthday x $$$

Lean4

theorem birthday_eq_pGameBirthday (x : Game) : ∃ y : PGame.{u}, ⟦y⟧ = x ∧ y.birthday = birthday x :=
  by
  refine csInf_mem (Set.image_nonempty.2 ?_)
  exact ⟨_, x.out_eq⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru