le_of_not_ge

Mathlib.Order.Defs.LinearOrder

URI: https://scilib.ai/kg/mathlib#le_of_not_ge

English

If not a ≤ b, then b ≤ a must hold (in a linear order).

Русский

Если не выполняется a ≤ b, то должно выполняться b ≤ a (в линейном порядке).

LaTeX

$$$ \\neg(a \\le b) \\rightarrow b \\le a$$$

Lean4

theorem le_of_not_ge : ¬a ≤ b → b ≤ a :=
  (le_total a b).resolve_left

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

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

Разделы

Аффилиация

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