nonpos

Mathlib.SetTheory.Game.Impartial

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

English

For an impartial G, 0 is not less than G: ¬(0 < G).

Русский

Для непредвзятой G ноль не меньше G: ¬(0 < G).

LaTeX

$$$\neg(0 < G)$$$

Lean4

theorem nonpos : ¬0 < G := by
  apply (lt_asymm · ?_)
  rwa [← neg_lt_neg_iff, neg_zero, ← lt_congr_right (neg_equiv_self G)]

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

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

Разделы

Аффилиация

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