mathlib3 documentation

order.circular

Circular order hierarchy #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 on order_dual α here. The instances has_le α → has_btw αᵒᵈ and has_lt α → has_sbtw αᵒᵈ 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, 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

Syntax typeclass for a betweenness relation.

Instances of this typeclass
Instances of other typeclasses for has_btw
  • has_btw.has_sizeof_inst
@[class]
structure has_sbtw (α : Type u_1) :
Type u_1

Syntax typeclass for a strict betweenness relation.

Instances of this typeclass
Instances of other typeclasses for has_sbtw
  • has_sbtw.has_sizeof_inst
@[class]
structure circular_preorder (α : Type u_1) :
Type u_1

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 of this typeclass
Instances of other typeclasses for circular_preorder
  • circular_preorder.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for circular_partial_order
  • circular_partial_order.has_sizeof_inst
@[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 of this typeclass
Instances of other typeclasses for circular_order
  • circular_order.has_sizeof_inst

Circular preorders #

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

Alias of btw_cyclic_right.

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

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 : α} :
theorem btw_of_sbtw {α : Type u_1} [circular_preorder α] {a b c : α} (h : has_sbtw.sbtw a b c) :
theorem has_sbtw.sbtw.btw {α : Type u_1} [circular_preorder α] {a b c : α} (h : has_sbtw.sbtw a b c) :

Alias of btw_of_sbtw.

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

Alias of not_btw_of_sbtw.

theorem not_sbtw_of_btw {α : Type u_1} [circular_preorder α] {a b c : α} (h : has_btw.btw a b c) :
theorem has_btw.btw.not_sbtw {α : Type u_1} [circular_preorder α] {a b c : α} (h : has_btw.btw a b c) :

Alias of not_sbtw_of_btw.

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

Alias of sbtw_of_btw_not_btw.

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

Alias of sbtw_cyclic_left.

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

Alias of sbtw_cyclic_right.

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

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

Alias of sbtw_trans_right.

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

Alias of sbtw_asymm.

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

Circular partial orders #

theorem has_btw.btw.antisymm {α : Type u_1} [circular_partial_order α] {a b c : α} (h : has_btw.btw a b c) :
has_btw.btw c b a a = b b = c c = a

Circular orders #

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

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 : α} :
@[simp]
theorem set.mem_cIoo {α : Type u_1} [circular_preorder α] {a b x : α} :
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 #

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

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

Equations
@[reducible]
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
@[reducible]

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