# Documentation

Mathlib.Order.Circular

# Circular order hierarchy #

This file defines circular preorders, circular partial orders and circular orders.

## Hierarchy #

• A ternary "betweenness" relation btw : α → α → α → Prop→ α → α → Prop→ α → Prop→ Prop forms a CircularOrder if it is
• reflexive: btw a a a
• cyclic: btw a b c → btw b c a→ btw b c a
• antisymmetric: btw a b c → btw c b a → a = b ∨ b = c ∨ c = a→ btw c b a → a = b ∨ b = c ∨ c = a→ a = b ∨ b = c ∨ c = a∨ b = c ∨ c = a∨ c = a
• total: btw a b c ∨ btw c b a∨ btw c b a along with a strict betweenness relation sbtw : α → α → α → Prop→ α → α → Prop→ α → Prop→ Prop which respects sbtw a b c ↔ btw a b c ∧ ¬ btw c b a↔ btw a b c ∧ ¬ btw c b a∧ ¬ btw c b a¬ btw c b a, analogously to how < and ≤≤ are related, and is
• transitive: sbtw a b c → sbtw b d c → sbtw a d c→ sbtw b d c → sbtw a d c→ sbtw a d c.
• A CircularPartialOrder drops totality.
• A CircularPreorder further drops antisymmetry.

The intuition is that a circular order is a circle and btw a b c means that going around clockwise from a you reach b before c (b is between a and c is meaningless on an unoriented circle). A circular partial order is several, potentially intersecting, circles. A circular preorder is like a circular partial order, but several points can coexist.

Note that the relations between CircularPreorder, CircularPartialOrder and CircularOrder are subtler than between Preorder, PartialOrder, LinearOrder. In particular, one cannot simply extend the btw of a CircularPartialOrder to make it a CircularOrder.

One can translate from usual orders to circular ones by "closing the necklace at infinity". See LE.toBtw and LT.toSBtw. Going the other way involves "cutting the necklace" or "rolling the necklace open".

## Examples #

Some concrete circular orders one encounters in the wild are ZMod n for 0 < n, Circle, Real.Angle...

## Main definitions #

• Set.cIcc: Closed-closed circular interval.
• Set.cIoo: Open-open circular interval.

## Notes #

There's an unsolved diamond on OrderDual α here. The instances LE α → Btw αᵒᵈ→ Btw αᵒᵈ and LT α → SBtw αᵒᵈ→ SBtw αᵒᵈ can each be inferred in two ways:

• LE αBtw αBtw αᵒᵈ vs LE αLE αᵒᵈBtw αᵒᵈ
• LT αSBtw αSBtw αᵒᵈ vs LT αLT αᵒᵈSBtw αᵒᵈ The fields are propeq, but not defeq. It is temporarily fixed by turning the circularizing instances into definitions.

## TODO #

Antisymmetry is quite weak in the sense that there's no way to discriminate which two points are equal. This prevents defining closed-open intervals cIco and cIoc in the neat =-less way. We currently haven't defined them at all.

What is the correct generality of "rolling the necklace" open? At least, this works for α × β× β and β × α× α where α is a circular order and β is a linear order.

What's next is to define circular groups and provide instances for ZMod n, the usual circle group Circle, Real.Angle, and RootsOfUnity M. What conditions do we need on M for this last one to work?

We should have circular order homomorphisms. The typical example is days_to_month : days_of_the_year →c months_of_the_year→c months_of_the_year which relates the circular order of days and the circular order of months. Is α →c β→c β a good notation?

## References #

• https://en.wikipedia.org/wiki/Cyclic_order
• https://en.wikipedia.org/wiki/Partial_cyclic_order

## Tags #

circular order, cyclic order, circularly ordered set, cyclically ordered set

class Btw (α : Type u_1) :
Type u_1
• Betweenness for circular orders. btw a b c states that b is between a and c (in that order).

btw : αααProp

Syntax typeclass for a betweenness relation.

Instances
class SBtw (α : Type u_1) :
Type u_1
• Strict betweenness for circular orders. sbtw a b c states that b is strictly between a and c (in that order).

sbtw : αααProp

Syntax typeclass for a strict betweenness relation.

Instances
class CircularPreorder (α : Type u_1) extends , :
Type u_1
• a is between a and a.

btw_refl : ∀ (a : α), btw a a a
• If b is between a and c, then c is between b and a. This is motivated by imagining three points on a circle.

btw_cyclic_left : ∀ {a b c : α}, btw a b cbtw b c a
• Strict betweenness is given by betweenness in one direction and non-betweenness in the other.

I.e., if b is between a and c but not between c and a, then we say b is strictly between a and c.

sbtw_iff_btw_not_btw : autoParam (∀ {a b c : α}, sbtw a b c btw a b c ¬btw c b a) _auto✝
• For any fixed c, fun a b ↦ sbtw a b c↦ sbtw a b c is a transitive relation.

I.e., given a b d c in that "order", if we have b strictly between a and c, and d strictly between b and c, then d is strictly between a and c.

sbtw_trans_left : ∀ {a b c d : α}, sbtw a b csbtw b d csbtw a d c

A circular preorder is the analogue of a preorder where you can loop around. ≤≤ and < are replaced by ternary relations btw and sbtw. btw is reflexive and cyclic. sbtw is transitive.

Instances
class CircularPartialOrder (α : Type u_1) extends :
Type u_1
• If b is between a and c and also between c and a, then at least one pair of points among a, b, c are identical.

btw_antisymm : ∀ {a b c : α}, btw a b cbtw c b aa = b b = c c = a

A circular partial order is the analogue of a partial order where you can loop around. ≤≤ and < are replaced by ternary relations btw and sbtw. btw is reflexive, cyclic and antisymmetric. sbtw is transitive.

Instances
class CircularOrder (α : Type u_1) extends :
Type u_1
• For any triple of points, the second is between the other two one way or another.

btw_total : ∀ (a b c : α), btw a b c btw c b a

A circular order is the analogue of a linear order where you can loop around. ≤≤ and < are replaced by ternary relations btw and sbtw. btw is reflexive, cyclic, antisymmetric and total. sbtw is transitive.

Instances

### Circular preorders #

theorem btw_rfl {α : Type u_1} [inst : ] {a : α} :
btw a a a
theorem Btw.btw.cyclic_left {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : btw a b c) :
btw b c a
theorem btw_cyclic_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : btw a b c) :
btw c a b
theorem Btw.btw.cyclic_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : btw a b c) :
btw c a b

Alias of btw_cyclic_right.

theorem btw_cyclic {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} :
btw a b c btw c a b

The order of the ↔↔ has been chosen so that rw btw_cyclic cycles to the right while rw ←btw_cyclic←btw_cyclic cycles to the left (thus following the prepended arrow).

theorem sbtw_iff_btw_not_btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} :
sbtw a b c btw a b c ¬btw c b a
theorem btw_of_sbtw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
btw a b c
theorem SBtw.sbtw.btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
btw a b c

Alias of btw_of_sbtw.

theorem not_btw_of_sbtw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
¬btw c b a
theorem SBtw.sbtw.not_btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
¬btw c b a

Alias of not_btw_of_sbtw.

theorem not_sbtw_of_btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : btw a b c) :
¬sbtw c b a
theorem Btw.btw.not_sbtw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : btw a b c) :
¬sbtw c b a

Alias of not_sbtw_of_btw.

theorem sbtw_of_btw_not_btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (habc : btw a b c) (hcba : ¬btw c b a) :
sbtw a b c
theorem Btw.btw.sbtw_of_not_btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (habc : btw a b c) (hcba : ¬btw c b a) :
sbtw a b c

Alias of sbtw_of_btw_not_btw.

theorem sbtw_cyclic_left {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
sbtw b c a
theorem SBtw.sbtw.cyclic_left {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
sbtw b c a

Alias of sbtw_cyclic_left.

theorem sbtw_cyclic_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
sbtw c a b
theorem SBtw.sbtw.cyclic_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
sbtw c a b

Alias of sbtw_cyclic_right.

theorem sbtw_cyclic {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} :
sbtw a b c sbtw c a b

The order of the ↔↔ has been chosen so that rw sbtw_cyclic cycles to the right while rw ←sbtw_cyclic←sbtw_cyclic cycles to the left (thus following the prepended arrow).

theorem SBtw.sbtw.trans_left {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} {d : α} (h : sbtw a b c) :
sbtw b d csbtw a d c
theorem sbtw_trans_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} {d : α} (hbc : sbtw a b c) (hcd : sbtw a c d) :
sbtw a b d
theorem SBtw.sbtw.trans_right {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} {d : α} (hbc : sbtw a b c) (hcd : sbtw a c d) :
sbtw a b d

Alias of sbtw_trans_right.

theorem sbtw_asymm {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
¬sbtw c b a
theorem SBtw.sbtw.not_sbtw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : sbtw a b c) :
¬sbtw c b a

Alias of sbtw_asymm.

theorem sbtw_irrefl_left_right {α : Type u_1} [inst : ] {a : α} {b : α} :
¬sbtw a b a
theorem sbtw_irrefl_left {α : Type u_1} [inst : ] {a : α} {b : α} :
¬sbtw a a b
theorem sbtw_irrefl_right {α : Type u_1} [inst : ] {a : α} {b : α} :
¬sbtw a b b
theorem sbtw_irrefl {α : Type u_1} [inst : ] (a : α) :
¬sbtw a a a

### Circular partial orders #

theorem Btw.btw.antisymm {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} (h : btw a b c) :
btw c b aa = b b = c c = a

### Circular orders #

theorem btw_refl_left_right {α : Type u_1} [inst : ] (a : α) (b : α) :
btw a b a
theorem btw_rfl_left_right {α : Type u_1} [inst : ] {a : α} {b : α} :
btw a b a
theorem btw_refl_left {α : Type u_1} [inst : ] (a : α) (b : α) :
btw a a b
theorem btw_rfl_left {α : Type u_1} [inst : ] {a : α} {b : α} :
btw a a b
theorem btw_refl_right {α : Type u_1} [inst : ] (a : α) (b : α) :
btw a b b
theorem btw_rfl_right {α : Type u_1} [inst : ] {a : α} {b : α} :
btw a b b
theorem sbtw_iff_not_btw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} :
sbtw a b c ¬btw c b a
theorem btw_iff_not_sbtw {α : Type u_1} [inst : ] {a : α} {b : α} {c : α} :
btw a b c ¬sbtw c b a

### Circular intervals #

def Set.cIcc {α : Type u_1} [inst : ] (a : α) (b : α) :
Set α

Closed-closed circular interval

Equations
def Set.cIoo {α : Type u_1} [inst : ] (a : α) (b : α) :
Set α

Open-open circular interval

Equations
@[simp]
theorem Set.mem_cIcc {α : Type u_1} [inst : ] {a : α} {b : α} {x : α} :
x Set.cIcc a b btw a x b
@[simp]
theorem Set.mem_cIoo {α : Type u_1} [inst : ] {a : α} {b : α} {x : α} :
x Set.cIoo a b sbtw a x b
theorem Set.left_mem_cIcc {α : Type u_1} [inst : ] (a : α) (b : α) :
theorem Set.right_mem_cIcc {α : Type u_1} [inst : ] (a : α) (b : α) :
theorem Set.compl_cIcc {α : Type u_1} [inst : ] {a : α} {b : α} :
theorem Set.compl_cIoo {α : Type u_1} [inst : ] {a : α} {b : α} :

### Circularizing instances #

def LE.toBtw (α : Type u_1) [inst : LE α] :
Btw α

The betweenness relation obtained from "looping around" ≤≤. See note [reducible non-instances].

Equations
def LT.toSBtw (α : Type u_1) [inst : LT α] :
SBtw α

The strict betweenness relation obtained from "looping around" <. See note [reducible non-instances].

Equations
def Preorder.toCircularPreorder (α : Type u_1) [inst : ] :

The circular preorder obtained from "looping around" a preorder. See note [reducible non-instances].

Equations
• One or more equations did not get rendered due to their size.
def PartialOrder.toCircularPartialOrder (α : Type u_1) [inst : ] :

The circular partial order obtained from "looping around" a partial order. See note [reducible non-instances].

Equations
def LinearOrder.toCircularOrder (α : Type u_1) [inst : ] :

The circular order obtained from "looping around" a linear order. See note [reducible non-instances].

Equations

### Dual constructions #

instance OrderDual.btw (α : Type u_1) [inst : Btw α] :
Equations
• = { btw := fun a b c => btw c b a }
instance OrderDual.sbtw (α : Type u_1) [inst : SBtw α] :
Equations
• = { sbtw := fun a b c => sbtw c b a }
instance OrderDual.circularPreorder (α : Type u_1) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance OrderDual.circularPartialOrder (α : Type u_1) [inst : ] :
Equations
instance OrderDual.instCircularOrderOrderDual (α : Type u_1) [inst : ] :
Equations