not_lt_zero

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

English

No element of WithZero α is strictly less than 0.

Русский

Ни один элемент WithZero α не строго меньше 0.

LaTeX

$$$ \neg (x < 0) $$$

Lean4

@[simp]
protected theorem not_lt_zero (a : WithZero α) : ¬a < 0 := by simp [lt_def]

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

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

Разделы

Аффилиация

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