@[simp]

theorem GameForm.birthday_eq_zero {x : GameForm} : Form.birthday x = 0 ↔ x = 0

noncomputable def GameForm.birthdayFinset : ℕ → Finset GameForm

Equations

• One or more equations did not get rendered due to their size.
• GameForm.birthdayFinset 0 = {0}

theorem GameForm.mem_birthdayFinset_succ {x : GameForm} {n : ℕ} : x ∈ birthdayFinset (n + 1) ↔ ∃ (l : Finset GameForm) (r : Finset GameForm), (l ⊆ birthdayFinset n ∧ r ⊆ birthdayFinset n) ∧ !{↑l | ↑r} = x

@[simp]

theorem GameForm.birthdayFinset_zero : birthdayFinset 0 = {0}

@[simp]

theorem GameForm.mem_birthdayFinset {x : GameForm} {n : ℕ} : x ∈ birthdayFinset n ↔ Form.birthday x ≤ ↑n