not_lt_zero'

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

English

For any a in a linear ordered monoid with zero, not (a < 0).

Русский

Для любого a в линейно упорядоченном моноиде с нулём не выполняется a < 0.

LaTeX

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

Lean4

@[simp]
theorem not_lt_zero' : ¬a < 0 :=
  not_lt_of_ge zero_le'

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

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

Разделы

Аффилиация

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