not_le_iff_lt_or_incompRel

Mathlib.Order.Comparable

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

English

¬(b ≤ a) is equivalent to a < b or IncompRel a b.

Русский

¬(b ≤ a) эквивалентно a < b или IncompRel a b.

LaTeX

$$¬(b ≤ a) \iff (a < b) \lor IncompRel(≤) a b$$

Lean4

theorem not_le_iff_lt_or_incompRel : ¬b ≤ a ↔ a < b ∨ IncompRel (· ≤ ·) a b :=
  by
  rw [lt_iff_le_not_ge, IncompRel]
  tauto

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

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

Разделы

Аффилиация

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