English
From a preorder (α, ≤) one constructs a circular preorder on α by defining btw(a,b,c) to be the cyclic inequalities a ≤ b ≤ c or b ≤ c ≤ a or c ≤ a ≤ b, and sbtw with strict inequalities in the same cyclic pattern; this yields a circular preorder structure on α.
Русский
Из preorder (α, ≤) строят циклический порядок на α, задавая btw(a,b,c) как циклические неравенства a ≤ b ≤ c или b ≤ c ≤ a или c ≤ a ≤ b, и sbtw аналогично с строгими неравенствами; получается циклический порядок на α.
LaTeX
$$$btw(a,b,c) := (a \le b \land b \le c) \lor (b \le c \land c \le a) \lor (c \le a \land a \le b),\quad sbtw(a,b,c) := (a < b \land b < c) \lor (b < c \land c < a) \lor (c < a \land a < b).$$$
Lean4
/-- The circular preorder obtained from "looping around" a preorder.
See note [reducible non-instances]. -/
abbrev toCircularPreorder (α : Type*) [Preorder α] : CircularPreorder α
where
btw a b c := a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
sbtw a b c := a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b
btw_refl _ := .inl ⟨le_rfl, le_rfl⟩
btw_cyclic_left {a b c} := .rotate
sbtw_trans_left
{a b c d} := by
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩) <;>
first
| refine .inl ?_; constructor <;> order
| refine .inr <| .inl ?_; constructor <;> order
| refine .inr <| .inr ?_; constructor <;> order
sbtw_iff_btw_not_btw
{a b c} := by
simp_rw [lt_iff_le_not_ge]
have h1 := le_trans a b c
have h2 := le_trans b c a
have h3 := le_trans c a b
grind
