lt_iff_le_not_ge

Mathlib.Order.Defs.PartialOrder

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

English

For all a,b in α, a < b iff a ≤ b and not b ≤ a.

Русский

Для любых a,b : α верно, что a < b тогда и только если a ≤ b и не (b ≤ a).

LaTeX

$$$a < b \\iff (a \\le b \\\\land \\\\lnot (b \\le a))$$$

Lean4

theorem lt_iff_le_not_ge : a < b ↔ a ≤ b ∧ ¬b ≤ a :=
  Preorder.lt_iff_le_not_ge _ _

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

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

Разделы

Аффилиация

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