not_gt

Mathlib.Order.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

protected theorem not_gt (hab : a = b) : ¬b < a :=
  hab.symm.not_lt

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

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

Разделы

Аффилиация

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