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

source
@[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
source
@[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
source
@[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
source
@[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
source
@[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 #

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

Alias of btw_cyclic_right.

source
theorem btw_cyclic {α : Type u_1} [circular_preorder α] {a b c : α} :
has_btw.btw a b c ↔ has_btw.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).

source
theorem sbtw_iff_btw_not_btw {α : Type u_1} [circular_preorder α] {a b c : α} :
has_sbtw.sbtw a b c ↔ has_btw.btw a b c ∧ ¬has_btw.btw c b a
source
theorem btw_of_sbtw {α : Type u_1} [circular_preorder α] {a b c : α} (h : has_sbtw.sbtw a b c) :
has_btw.btw a b c
source
theorem has_sbtw.sbtw.btw {α : Type u_1} [circular_preorder α] {a b c : α} (h : has_sbtw.sbtw a b c) :
has_btw.btw a b c

Alias of btw_of_sbtw.

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

Alias of not_btw_of_sbtw.

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

Alias of not_sbtw_of_btw.

source
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) :
has_sbtw.sbtw a b c
source
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) :
has_sbtw.sbtw a b c

Alias of sbtw_of_btw_not_btw.

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

Alias of sbtw_cyclic_left.

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

Alias of sbtw_cyclic_right.

source
theorem sbtw_cyclic {α : Type u_1} [circular_preorder α] {a b c : α} :
has_sbtw.sbtw a b c ↔ has_sbtw.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).

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

Alias of sbtw_trans_right.

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

Alias of sbtw_asymm.

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

Circular partial orders #

source
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 #

source
theorem btw_refl_left_right {α : Type u_1} [circular_order α] (a b : α) :
has_btw.btw a b a
source
theorem btw_rfl_left_right {α : Type u_1} [circular_order α] {a b : α} :
has_btw.btw a b a
source
theorem btw_refl_left {α : Type u_1} [circular_order α] (a b : α) :
has_btw.btw a a b
source
theorem btw_rfl_left {α : Type u_1} [circular_order α] {a b : α} :
has_btw.btw a a b
source
theorem btw_refl_right {α : Type u_1} [circular_order α] (a b : α) :
has_btw.btw a b b
source
theorem btw_rfl_right {α : Type u_1} [circular_order α] {a b : α} :
has_btw.btw a b b
source
theorem sbtw_iff_not_btw {α : Type u_1} [circular_order α] {a b c : α} :
has_sbtw.sbtw a b c ↔ ¬has_btw.btw c b a
source
theorem btw_iff_not_sbtw {α : Type u_1} [circular_order α] {a b c : α} :
has_btw.btw a b c ↔ ¬has_sbtw.sbtw c b a

Circular intervals #

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

Closed-closed circular interval

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

Open-open circular interval

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

Circularizing instances #

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

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

Equations
source
@[reducible]
def has_lt.to_has_sbtw (α : Type u_1) [has_lt α] :
has_sbtw α

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

Equations
source
@[reducible]
def preorder.to_circular_preorder (α : Type u_1) [preorder α] :
circular_preorder α

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

Equations
source
@[reducible]
def partial_order.to_circular_partial_order (α : Type u_1) [partial_order α] :
circular_partial_order α

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

Equations
source
@[reducible]
def linear_order.to_circular_order (α : Type u_1) [linear_order α] :
circular_order α

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

Equations

Dual constructions #

source
@[protected, instance]
def order_dual.has_btw (α : Type u_1) [has_btw α] :
has_btw αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_sbtw (α : Type u_1) [has_sbtw α] :
has_sbtw αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.circular_preorder (α : Type u_1) [h : circular_preorder α] :
circular_preorder αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.circular_partial_order (α : Type u_1) [circular_partial_order α] :
circular_partial_order αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.circular_order (α : Type u_1) [circular_order α] :
circular_order αᵒᵈ
Equations