mathlib documentation

order.circular

Circular order hierarchy #

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

Hierarchy #

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 circular_preorder, circular_partial_order and circular_order are subtler than between preorder, partial_order, linear_order. In particular, one cannot simply extend the btw of a circular_partial_order to make it a circular_order.

One can translate from usual orders to circular ones by "closing the necklace at infinity". See has_le.to_has_btw and has_lt.to_has_sbtw. 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 #

Notes #

There's an unsolved diamond here. The instances has_le α → has_btw (order_dual α) and has_lt α → has_sbtw (order_dual α) can each be inferred in two ways:

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 roots_of_unity 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 which relates the circular order of days and the circular order of months. Is α →c β a good notation?

References #

Tags #

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

@[class]
structure has_btw (α : Type u_1) :
Type u_1
  • btw : α → α → α → Prop

Syntax typeclass for a betweenness relation.

Instances
@[class]
structure has_sbtw (α : Type u_1) :
Type u_1
  • sbtw : α → α → α → Prop

Syntax typeclass for a strict betweenness relation.

Instances
@[class]
structure circular_preorder (α : Type u_1) :
Type u_1
  • to_has_btw : has_btw α
  • to_has_sbtw : has_sbtw α
  • btw_refl : ∀ (a : α), btw a a a
  • btw_cyclic_left : ∀ {a b c : α}, btw a b cbtw b c a
  • sbtw_iff_btw_not_btw : ∀ {a b c : α}, sbtw a b c btw a b c ¬btw c b a . "order_laws_tac"
  • 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]
structure circular_partial_order (α : Type u_1) :
Type u_1

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]
structure circular_order (α : Type u_1) :
Type u_1

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} [circular_preorder α] {a : α} :
btw a a a
theorem has_btw.btw.cyclic_left {α : Type u_1} [circular_preorder α] {a b c : α} (h : btw a b c) :
btw b c a
theorem btw_cyclic_right {α : Type u_1} [circular_preorder α] {a b c : α} (h : btw a b c) :
btw c a b
theorem has_btw.btw.cyclic_right {α : Type u_1} [circular_preorder α] {a b c : α} (h : btw a b c) :
btw c a b

Alias of btw_cyclic_right.

theorem btw_cyclic {α : Type u_1} [circular_preorder α] {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 cycles to the left (thus following the prepended arrow).

theorem sbtw_iff_btw_not_btw {α : Type u_1} [circular_preorder α] {a b c : α} :
sbtw a b c btw a b c ¬btw c b a
theorem btw_of_sbtw {α : Type u_1} [circular_preorder α] {a b c : α} (h : sbtw a b c) :
btw a b c
theorem has_sbtw.sbtw.btw {α : Type u_1} [circular_preorder α] {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} [circular_preorder α] {a b c : α} (h : sbtw a b c) :
¬btw c b a
theorem has_sbtw.sbtw.not_btw {α : Type u_1} [circular_preorder α] {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} [circular_preorder α] {a b c : α} (h : btw a b c) :
¬sbtw c b a
theorem has_btw.btw.not_sbtw {α : Type u_1} [circular_preorder α] {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} [circular_preorder α] {a b c : α} (habc : btw a b c) (hcba : ¬btw c b a) :
sbtw a b c
theorem has_btw.btw.sbtw_of_not_btw {α : Type u_1} [circular_preorder α] {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} [circular_preorder α] {a b c : α} (h : sbtw a b c) :
sbtw b c a
theorem has_sbtw.sbtw.cyclic_left {α : Type u_1} [circular_preorder α] {a b c : α} (h : sbtw a b c) :
sbtw b c a

Alias of sbtw_cyclic_left.

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

Alias of sbtw_cyclic_right.

theorem sbtw_cyclic {α : Type u_1} [circular_preorder α] {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 cycles to the left (thus following the prepended arrow).

theorem has_sbtw.sbtw.trans_left {α : Type u_1} [circular_preorder α] {a b c d : α} (h : sbtw a b c) :
sbtw b d csbtw a d c
theorem sbtw_trans_right {α : Type u_1} [circular_preorder α] {a b c d : α} (hbc : sbtw a b c) (hcd : sbtw a c d) :
sbtw a b d
theorem has_sbtw.sbtw.trans_right {α : Type u_1} [circular_preorder α] {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} [circular_preorder α] {a b c : α} (h : sbtw a b c) :
¬sbtw c b a
theorem has_sbtw.sbtw.not_sbtw {α : Type u_1} [circular_preorder α] {a b c : α} (h : sbtw a b c) :
¬sbtw c b a

Alias of sbtw_asymm.

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

Circular partial orders #

theorem has_btw.btw.antisymm {α : Type u_1} [circular_partial_order α] {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} [circular_order α] (a b : α) :
btw a b a
theorem btw_rfl_left_right {α : Type u_1} [circular_order α] {a b : α} :
btw a b a
theorem btw_refl_left {α : Type u_1} [circular_order α] (a b : α) :
btw a a b
theorem btw_rfl_left {α : Type u_1} [circular_order α] {a b : α} :
btw a a b
theorem btw_refl_right {α : Type u_1} [circular_order α] (a b : α) :
btw a b b
theorem btw_rfl_right {α : Type u_1} [circular_order α] {a b : α} :
btw a b b
theorem sbtw_iff_not_btw {α : Type u_1} [circular_order α] {a b c : α} :
sbtw a b c ¬btw c b a
theorem btw_iff_not_sbtw {α : Type u_1} [circular_order α] {a b c : α} :
btw a b c ¬sbtw c b a

Circular intervals #

def set.cIcc {α : Type u_1} [circular_preorder α] (a b : α) :
set α

Closed-closed circular interval

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

Open-open circular interval

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

Circularizing instances #

def has_le.to_has_btw (α : Type u_1) [has_le α] :

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

Equations
def has_lt.to_has_sbtw (α : Type u_1) [has_lt α] :

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

Equations

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

Equations

Dual constructions #

@[protected, instance]
def order_dual.has_btw (α : Type u_1) [has_btw α] :
Equations
@[protected, instance]
def order_dual.has_sbtw (α : Type u_1) [has_sbtw α] :
Equations