btw_iff

Mathlib.Order.Circular

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

Lean4

/-- The following lemmas are about the non-instances `LE.toBtw`, `LT.toSBtw` and
`LinearOrder.toCircularOrder`. -/
theorem btw_iff [LE α] : btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b :=
  .rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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