le_birthday

Mathlib.SetTheory.Game.Birthday

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

← MathLib Explorer

English

For any game x, x ≤ (birthday(x)).toGame.

Русский

Для любого x: x ≤ (birthday(x)).toGame.

LaTeX

$$$x \le (x.birthday).toGame$$$

Lean4

theorem le_birthday (x : Game) : x ≤ x.birthday.toGame :=
  by
  let ⟨y, hy₁, hy₂⟩ := birthday_eq_pGameBirthday x
  rw [← hy₁]
  apply (y.le_birthday).trans
  rw [toPGame_le_iff, hy₁, hy₂]

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

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

Разделы

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

Аффилиация

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