neg_birthday_le

Mathlib.SetTheory.Game.Birthday

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.neg_birthday_le

English

For all x, -x.birthday.toPGame ≤ x.

Русский

Для любого x, -x.birthday.toPGame ≤ x.

LaTeX

$$$ -x.birthday.toPGame \le x $$$

Lean4

theorem neg_birthday_le : -x.birthday.toPGame ≤ x := by simpa only [birthday_neg, ← neg_le_iff] using le_birthday (-x)

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

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

Разделы

Аффилиация

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