birthday_sub_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_sub_le (x y : Game) : (x - y).birthday ≤ x.birthday ♯ y.birthday :=
  by
  apply (birthday_add_le x _).trans_eq
  rw [birthday_neg]
    /- The bound `(x * y).birthday ≤ x.birthday ⨳ y.birthday` is currently an open problem. See
      https://mathoverflow.net/a/476829/147705. -/

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