gt_or_lt

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#LT.lt.gt_or_lt

English

If a ≠ b, then ¬(a ≤ b) or ¬(b ≤ a).

Русский

Если a ≠ b, то либо не выполняется a ≤ b, либо не выполняется b ≤ a.

LaTeX

$$$a \\neq b \\rightarrow \\lnot (a \\le b) \\lor \\lnot (b \\le a)$$$

Lean4

theorem gt_or_lt (h : a < b) (c : α) : a < c ∨ c < b :=
  (le_or_gt b c).imp h.trans_le id

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

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

Разделы

Аффилиация

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