toBtw

Mathlib.Order.Circular

URI: https://scilib.ai/kg/mathlib#LE.toBtw

Lean4

/-- The betweenness relation obtained from "looping around" `≤`.
See note [reducible non-instances]. -/
abbrev toBtw (α : Type*) [LE α] : Btw α where btw a b c := a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b

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

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

Разделы

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

Аффилиация

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