lt_or_ge

Mathlib.Order.Defs.LinearOrder

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

English

Let α be a linear order. Then either a < b or b ≤ a.

Русский

Пусть α — линейный порядок. Тогда либо a < b, либо b ≤ a.

LaTeX

$$$ a < b \\lor b \\le a $$$

Lean4

theorem lt_or_ge (a b : α) : a < b ∨ b ≤ a :=
  if hba : b ≤ a then Or.inr hba else Or.inl <| lt_of_not_ge hba

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

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

Разделы

Аффилиация

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