not_le_or_not_ge

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#Ne.not_le_or_not_ge

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 not_le_or_not_ge (h : a ≠ b) : ¬a ≤ b ∨ ¬b ≤ a :=
  not_and_or.1 <| le_antisymm_iff.not.1 h

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

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

Разделы

Аффилиация

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