not_lt

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Eq.not_lt

English

If a = b, then not (a < b).

Русский

Если a = b, то не (a < b).

LaTeX

$$$a = b \\to \\neg(a < b)$$$

Lean4

protected theorem not_lt (hab : a = b) : ¬a < b := fun h' ↦ h'.ne hab

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

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

Разделы

Аффилиация

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