birthday_add_le — Mathlib

English

For all x,y, the birthday of x+y is at most the natural sum of their birthdays.

Русский

Для любых x,y день рождения x+y не превосходит естественной суммы их дней рождения.

LaTeX

$$$\operatorname{birthday}(x + y) \le \operatorname{birthday}(x) ⊞ \operatorname{birthday}(y)$$$

Lean4

theorem birthday_add_le (x y : Game) : (x + y).birthday ≤ x.birthday ♯ y.birthday :=
  by
  let ⟨a, ha₁, ha₂⟩ := birthday_eq_pGameBirthday x
  let ⟨b, hb₁, hb₂⟩ := birthday_eq_pGameBirthday y
  rw [← ha₂, ← hb₂, ← ha₁, ← hb₁, ← PGame.birthday_add]
  exact birthday_quot_le_pGameBirthday _

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