not_lt_zero

Mathlib.SetTheory.Nimber.Basic

URI: https://scilib.ai/kg/mathlib#Nimber.not_lt_zero

English

No nimber is strictly less than zero: for all a, not (a < 0).

Русский

Ни один Nimber не меньше нуля: для всех a верно ¬(a < 0).

LaTeX

$$$\neg (a < 0)$$$

Lean4

protected theorem not_lt_zero (a : Nimber) : ¬a < 0 :=
  Ordinal.not_lt_zero a

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

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

Разделы

Аффилиация

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