Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2021 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
! This file was ported from Lean 3 source module order.circular
! leanprover-community/mathlib commit 213b0cff7bc5ab6696ee07cceec80829ce42efec
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Basic
/-!
# Circular order hierarchy
This file defines circular preorders, circular partial orders and circular orders.
## Hierarchy
* A ternary "betweenness" relation `btw : α → α → α → Prop` forms a `CircularOrder` if it is
- reflexive: `btw a a a`
- cyclic: `btw a b c → btw b c a`
- antisymmetric: `btw a b c → btw c b a → a = b ∨ b = c ∨ c = a`
- total: `btw a b c ∨ btw c b a`
along with a strict betweenness relation `sbtw : α → α → α → Prop` which respects
`sbtw a b c ↔ btw a b c ∧ ¬ 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`.
* 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 αᵒᵈ` and
`LT α → 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`, 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` which relates the circular order of days
and the circular order of months. Is `α →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
-/
/-- Syntax typeclass for a betweenness relation. -/
class Btw ( α : Type _ ) where
/-- Betweenness for circular orders. `btw a b c` states that `b` is between `a` and `c` (in that
order). -/
btw : {α : Type u_1} → [self : Btw α α → α → α → Prop : α → α → α → Prop
#align has_btw Btw
export Btw (btw)
/-- Syntax typeclass for a strict betweenness relation. -/
class SBtw ( α : Type _ ) where
/-- Strict betweenness for circular orders. `sbtw a b c` states that `b` is strictly between `a`
and `c` (in that order). -/
sbtw : α → α → α → Prop
#align has_sbtw SBtw
export SBtw (sbtw)
/-- 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.
-/
class CircularPreorder ( α : Type _ ) extends Btw α , SBtw α where
/-- `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 c → btw b c a
sbtw := fun a b c => btw a b c ∧ ¬ btw c b 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 { a b c : α } : sbtw a b c ↔ btw a b c ∧ ¬ btw c b a := by intros ; rfl
/-- For any fixed `c`, `fun a b ↦ 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 c → sbtw b d c → sbtw a d c
#align circular_preorder CircularPreorder
export CircularPreorder (btw_refl btw_cyclic_left sbtw_trans_left)
/-- 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. -/
class CircularPartialOrder : Type u_1 → Type u_1 ( α : Type _ ) extends CircularPreorder : Type ?u.222 → Type ?u.222 α where
/-- 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 c → btw c b a → a = b ∨ b = c ∨ c = a
#align circular_partial_order CircularPartialOrder : Type u_1 → Type u_1
export CircularPartialOrder (btw_antisymm)
/-- 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. -/
class CircularOrder ( α : Type _ ) extends CircularPartialOrder : Type ?u.301 → Type ?u.301 α where
/-- 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
#align circular_order CircularOrder
export CircularOrder (btw_total)
/-! ### Circular preorders -/
section CircularPreorder
variable { α : Type _ } [ CircularPreorder : Type ?u.1012 → Type ?u.1012 α ]
theorem btw_rfl { a : α } : btw : {α : Type ?u.385} → [self : Btw α α → α → α → Prop a a a :=
btw_refl _
#align btw_rfl btw_rfl
-- TODO: `alias` creates a def instead of a lemma.
-- alias btw_cyclic_left ← has_btw.btw.cyclic_left
theorem Btw.btw.cyclic_left : ∀ {a b c : α }, btw a b c btw b c a Btw.btw.cyclic_left { a b c : α } ( h : btw : {α : Type ?u.440} → [self : Btw α α → α → α → Prop a b c ) : btw : {α : Type ?u.462} → [self : Btw α α → α → α → Prop b c a :=
btw_cyclic_left h
#align has_btw.btw.cyclic_left Btw.btw.cyclic_left
theorem btw_cyclic_right { a b c : α } ( h : btw : {α : Type ?u.518} → [self : Btw α α → α → α → Prop a b c ) : btw : {α : Type ?u.540} → [self : Btw α α → α → α → Prop c a b :=
h . cyclic_left . cyclic_left
#align btw_cyclic_right btw_cyclic_right
alias btw_cyclic_right ← Btw.btw.cyclic_right
#align has_btw.btw.cyclic_right Btw.btw.cyclic_right
/-- 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 btw_cyclic { a b c : α } : btw : {α : Type ?u.605} → [self : Btw α α → α → α → Prop a b c ↔ btw : {α : Type ?u.618} → [self : Btw α α → α → α → Prop c a b :=
⟨ btw_cyclic_right , btw_cyclic_left ⟩
#align btw_cyclic btw_cyclic
theorem sbtw_iff_btw_not_btw { a b c : α } : sbtw : {α : Type ?u.684} → [self : SBtw α α → α → α → Prop a b c ↔ btw : {α : Type ?u.697} → [self : Btw α α → α → α → Prop a b c ∧ ¬ btw : {α : Type ?u.707} → [self : Btw α α → α → α → Prop c b a :=
CircularPreorder.sbtw_iff_btw_not_btw
#align sbtw_iff_btw_not_btw sbtw_iff_btw_not_btw
theorem btw_of_sbtw { a b c : α } ( h : sbtw : {α : Type ?u.754} → [self : SBtw α α → α → α → Prop a b c ) : btw : {α : Type ?u.776} → [self : Btw α α → α → α → Prop a b c :=
( sbtw_iff_btw_not_btw . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 1 : ∀ {a b : Prop }, a ∧ b a
#align btw_of_sbtw btw_of_sbtw
alias btw_of_sbtw ← SBtw.sbtw.btw
#align has_sbtw.sbtw.btw SBtw.sbtw.btw
theorem not_btw_of_sbtw : ∀ {a b c : α }, sbtw a b c ¬ btw c b a not_btw_of_sbtw { a b c : α } ( h : sbtw : {α : Type ?u.847} → [self : SBtw α α → α → α → Prop a b c ) : ¬ btw : {α : Type ?u.869} → [self : Btw α α → α → α → Prop c b a :=
( sbtw_iff_btw_not_btw . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 2 : ∀ {a b : Prop }, a ∧ b b
#align not_btw_of_sbtw not_btw_of_sbtw
alias not_btw_of_sbtw ← SBtw.sbtw.not_btw
#align has_sbtw.sbtw.not_btw SBtw.sbtw.not_btw
theorem not_sbtw_of_btw : ∀ {a b c : α }, btw a b c ¬ sbtw c b a not_sbtw_of_btw { a b c : α } ( h : btw : {α : Type ?u.934} → [self : Btw α α → α → α → Prop a b c ) : ¬ sbtw : {α : Type ?u.956} → [self : SBtw α α → α → α → Prop c b a := fun h' => h' . not_btw h
#align not_sbtw_of_btw not_sbtw_of_btw
alias not_sbtw_of_btw ← Btw.btw.not_sbtw
#align has_btw.btw.not_sbtw Btw.btw.not_sbtw
theorem sbtw_of_btw_not_btw : ∀ {a b c : α }, btw a b c ¬ btw c b a sbtw a b c sbtw_of_btw_not_btw { a b c : α } ( habc : btw : {α : Type ?u.1021} → [self : Btw α α → α → α → Prop a b c ) ( hcba : ¬ btw : {α : Type ?u.1043} → [self : Btw α α → α → α → Prop c b a ) : sbtw : {α : Type ?u.1048} → [self : SBtw α α → α → α → Prop a b c :=
sbtw_iff_btw_not_btw . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ habc , hcba ⟩
#align sbtw_of_btw_not_btw sbtw_of_btw_not_btw
alias sbtw_of_btw_not_btw ← Btw.btw.sbtw_of_not_btw
#align has_btw.btw.sbtw_of_not_btw Btw.btw.sbtw_of_not_btw
theorem sbtw_cyclic_left : ∀ {a b c : α }, sbtw a b c sbtw b c a sbtw_cyclic_left { a b c : α } ( h : sbtw : {α : Type ?u.1127} → [self : SBtw α α → α → α → Prop a b c ) : sbtw : {α : Type ?u.1149} → [self : SBtw α α → α → α → Prop b c a :=
h . btw . cyclic_left . sbtw_of_not_btw fun h' => h . not_btw h' . cyclic_left
#align sbtw_cyclic_left sbtw_cyclic_left
alias sbtw_cyclic_left ← SBtw.sbtw.cyclic_left
#align has_sbtw.sbtw.cyclic_left SBtw.sbtw.cyclic_left
theorem sbtw_cyclic_right { a b c : α } ( h : sbtw : {α : Type ?u.1256} → [self : SBtw α α → α → α → Prop a b c ) : sbtw : {α : Type ?u.1278} → [self : SBtw α α → α → α → Prop c a b :=
h . cyclic_left . cyclic_left
#align sbtw_cyclic_right sbtw_cyclic_right
alias sbtw_cyclic_right ← SBtw.sbtw.cyclic_right
#align has_sbtw.sbtw.cyclic_right SBtw.sbtw.cyclic_right
/-- 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 sbtw_cyclic { a b c : α } : sbtw : {α : Type ?u.1343} → [self : SBtw α α → α → α → Prop a b c ↔ sbtw : {α : Type ?u.1356} → [self : SBtw α α → α → α → Prop c a b :=
⟨ sbtw_cyclic_right , sbtw_cyclic_left ⟩
#align sbtw_cyclic sbtw_cyclic
-- TODO: `alias` creates a def instead of a lemma.
-- alias btw_trans_left ← has_btw.btw.trans_left
theorem SBtw.sbtw.trans_left : ∀ {a b c d : α }, sbtw a b c sbtw b d c sbtw a d c SBtw.sbtw.trans_left { a b c d : α } ( h : sbtw : {α : Type ?u.1424} → [self : SBtw α α → α → α → Prop a b c ) : sbtw : {α : Type ?u.1447} → [self : SBtw α α → α → α → Prop b d c → sbtw : {α : Type ?u.1458} → [self : SBtw α α → α → α → Prop a d c :=
sbtw_trans_left h
#align has_sbtw.sbtw.trans_left SBtw.sbtw.trans_left
theorem sbtw_trans_right { a b c d : α } ( hbc : sbtw : {α : Type ?u.1526} → [self : SBtw α α → α → α → Prop a b c ) ( hcd : sbtw : {α : Type ?u.1548} → [self : SBtw α α → α → α → Prop a c d ) : sbtw : {α : Type ?u.1560} → [self : SBtw α α → α → α → Prop a b d :=
( hbc . cyclic_left . trans_left hcd . cyclic_left ). cyclic_right
#align sbtw_trans_right sbtw_trans_right
alias sbtw_trans_right ← SBtw.sbtw.trans_right
#align has_sbtw.sbtw.trans_right SBtw.sbtw.trans_right
theorem sbtw_asymm : ∀ {a b c : α }, sbtw a b c ¬ sbtw c b a sbtw_asymm { a b c : α } ( h : sbtw : {α : Type ?u.1658} → [self : SBtw α α → α → α → Prop a b c ) : ¬ sbtw : {α : Type ?u.1680} → [self : SBtw α α → α → α → Prop c b a :=
h . btw . not_sbtw
#align sbtw_asymm sbtw_asymm
alias sbtw_asymm ← SBtw.sbtw.not_sbtw
#align has_sbtw.sbtw.not_sbtw SBtw.sbtw.not_sbtw
theorem sbtw_irrefl_left_right { a b : α } : ¬ sbtw : {α : Type ?u.1744} → [self : SBtw α α → α → α → Prop a b a := fun h => h . not_btw h . btw
#align sbtw_irrefl_left_right sbtw_irrefl_left_right
theorem sbtw_irrefl_left : ∀ {a b : α }, ¬ sbtw a a b sbtw_irrefl_left { a b : α } : ¬ sbtw : {α : Type ?u.1816} → [self : SBtw α α → α → α → Prop a a b := fun h => sbtw_irrefl_left_right h . cyclic_left
#align sbtw_irrefl_left sbtw_irrefl_left
theorem sbtw_irrefl_right : ∀ {a b : α }, ¬ sbtw a b b sbtw_irrefl_right { a b : α } : ¬ sbtw : {α : Type ?u.1888} → [self : SBtw α α → α → α → Prop a b b := fun h => sbtw_irrefl_left_right h . cyclic_right
#align sbtw_irrefl_right sbtw_irrefl_right
theorem sbtw_irrefl : ∀ (a : α ), ¬ sbtw a a a sbtw_irrefl ( a : α ) : ¬ sbtw : {α : Type ?u.1958} → [self : SBtw α α → α → α → Prop a a a :=
sbtw_irrefl_left_right
#align sbtw_irrefl sbtw_irrefl
end CircularPreorder
/-! ### Circular partial orders -/
section CircularPartialOrder
variable { α : Type _ } [ CircularPartialOrder : Type ?u.2000 → Type ?u.2000 α ]
-- TODO: `alias` creates a def instead of a lemma.
-- alias btw_antisymm ← has_btw.btw.antisymm
theorem Btw.btw.antisymm : ∀ {a b c : α }, btw a b c btw c b a a = b ∨ b = c ∨ c = a Btw.btw.antisymm { a b c : α } ( h : btw : {α : Type ?u.2015} → [self : Btw α α → α → α → Prop a b c ) : btw : {α : Type ?u.2048} → [self : Btw α α → α → α → Prop c b a → a = b ∨ b = c ∨ c = a :=
btw_antisymm h
#align has_btw.btw.antisymm Btw.btw.antisymm
end CircularPartialOrder
/-! ### Circular orders -/
section CircularOrder
variable { α : Type _ } [ CircularOrder : Type ?u.2650 → Type ?u.2650 α ]
theorem btw_refl_left_right : ∀ (a b : α ), btw a b a btw_refl_left_right ( a b : α ) : btw : {α : Type ?u.2123} → [self : Btw α α → α → α → Prop a b a :=
( or_self_iff : ∀ (p : Prop ), p ∨ p ↔ p _ ). 1 : ∀ {a b : Prop }, (a ↔ b a → b ( btw_total a b a )
#align btw_refl_left_right btw_refl_left_right
theorem btw_rfl_left_right : ∀ {a b : α }, btw a b a btw_rfl_left_right { a b : α } : btw : {α : Type ?u.2194} → [self : Btw α α → α → α → Prop a b a :=
btw_refl_left_right _ _
#align btw_rfl_left_right btw_rfl_left_right
theorem btw_refl_left ( a b : α ) : btw : {α : Type ?u.2267} → [self : Btw α α → α → α → Prop a a b :=
btw_rfl_left_right . cyclic_right
#align btw_refl_left btw_refl_left
theorem btw_rfl_left : ∀ {a b : α }, btw a a b btw_rfl_left { a b : α } : btw : {α : Type ?u.2389} → [self : Btw α α → α → α → Prop a a b :=
btw_refl_left _ _
#align btw_rfl_left btw_rfl_left
theorem btw_refl_right : ∀ (a b : α ), btw a b b btw_refl_right ( a b : α ) : btw : {α : Type ?u.2462} → [self : Btw α α → α → α → Prop a b b :=
btw_rfl_left_right . cyclic_left
#align btw_refl_right btw_refl_right
theorem btw_rfl_right : ∀ {a b : α }, btw a b b btw_rfl_right { a b : α } : btw : {α : Type ?u.2584} → [self : Btw α α → α → α → Prop a b b :=
btw_refl_right _ _
#align btw_rfl_right btw_rfl_right
theorem sbtw_iff_not_btw : ∀ {a b c : α }, sbtw a b c ↔ ¬ btw c b a sbtw_iff_not_btw { a b c : α } : sbtw : {α : Type ?u.2659} → [self : SBtw α α → α → α → Prop a b c ↔ ¬ btw : {α : Type ?u.2681} → [self : Btw α α → α → α → Prop c b a := by
rw [ sbtw_iff_btw_not_btw ]
exact and_iff_right_of_imp : ∀ {b a : Prop }, (b → a a ∧ b ↔ b ( btw_total _ _ _ ). resolve_left : ∀ {a b : Prop }, a ∨ b ¬ a b resolve_left
#align sbtw_iff_not_btw sbtw_iff_not_btw
theorem btw_iff_not_sbtw : ∀ {a b c : α }, btw a b c ↔ ¬ sbtw c b a btw_iff_not_sbtw { a b c : α } : btw : {α : Type ?u.2818} → [self : Btw α α → α → α → Prop a b c ↔ ¬ sbtw : {α : Type ?u.2840} → [self : SBtw α α → α → α → Prop c b a :=
iff_not_comm : ∀ {a b : Prop }, (a ↔ ¬ b ↔ (b ↔ ¬ a . 1 : ∀ {a b : Prop }, (a ↔ b a → b sbtw_iff_not_btw
#align btw_iff_not_sbtw btw_iff_not_sbtw
end CircularOrder
/-! ### Circular intervals -/
namespace Set
section CircularPreorder
variable { α : Type _ } [ CircularPreorder : Type ?u.2897 → Type ?u.2897 α ]
/-- Closed-closed circular interval -/
def cIcc ( a b : α ) : Set α :=
{ x | btw : {α : Type ?u.2917} → [self : Btw α α → α → α → Prop a x b }
#align set.cIcc Set.cIcc
/-- Open-open circular interval -/
def cIoo ( a b : α ) : Set α :=
{ x | sbtw : {α : Type ?u.2972} → [self : SBtw α α → α → α → Prop a x b }
#align set.cIoo Set.cIoo
@[ simp ]
theorem mem_cIcc : ∀ {a b x : α }, x ∈ cIcc a b ↔ btw a x b mem_cIcc { a b x : α } : x ∈ cIcc a b ↔ btw : {α : Type ?u.3043} → [self : Btw α α → α → α → Prop a x b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align set.mem_cIcc Set.mem_cIcc
@[ simp ]
theorem mem_cIoo : ∀ {a b x : α }, x ∈ cIoo a b ↔ sbtw a x b mem_cIoo { a b x : α } : x ∈ cIoo a b ↔ sbtw : {α : Type ?u.3135} → [self : SBtw α α → α → α → Prop a x b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align set.mem_cIoo Set.mem_cIoo
end CircularPreorder
section CircularOrder
variable { α : Type _ } [ CircularOrder : Type ?u.3287 → Type ?u.3287 α ]
theorem left_mem_cIcc : ∀ (a b : α ), a ∈ cIcc a b left_mem_cIcc ( a b : α ) : a ∈ cIcc a b :=
btw_rfl_left
#align set.left_mem_cIcc Set.left_mem_cIcc
theorem right_mem_cIcc ( a b : α ) : b ∈ cIcc a b :=
btw_rfl_right
#align set.right_mem_cIcc Set.right_mem_cIcc
theorem compl_cIcc { a b : α } : cIcc a b ᶜ = cIoo b a := by
ext
rw [ Set.mem_cIoo , sbtw_iff_not_btw ]
rfl
#align set.compl_cIcc Set.compl_cIcc
theorem compl_cIoo { a b : α } : cIoo a b ᶜ = cIcc b a := by
ext
rw [ Set.mem_cIcc , btw_iff_not_sbtw ]
rfl
#align set.compl_cIoo Set.compl_cIoo
end CircularOrder
end Set
/-! ### Circularizing instances -/
/-- The betweenness relation obtained from "looping around" `≤`.
See note [reducible non-instances]. -/
@[reducible]
def LE.toBtw : (α : Type u_1) → [inst : LE α Btw α LE.toBtw ( α : Type _ ) [ LE α ] : Btw α where
btw a b c := a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b
#align has_le.to_has_btw LE.toBtw : (α : Type u_1) → [inst : LE α Btw α
/-- The strict betweenness relation obtained from "looping around" `<`.
See note [reducible non-instances]. -/
@[reducible]
def LT.toSBtw : (α : Type ?u.3876) → [inst : LT α SBtw α LT.toSBtw ( α : Type _ ) [ LT α ] : SBtw α where
sbtw a b c := a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b
#align has_lt.to_has_sbtw LT.toSBtw : (α : Type u_1) → [inst : LT α SBtw α
/-- The circular preorder obtained from "looping around" a preorder.
See note [reducible non-instances]. -/
@[reducible]
def Preorder.toCircularPreorder ( α : Type _ ) [ Preorder α ] : CircularPreorder : Type ?u.3970 → Type ?u.3970 α 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 a := Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ le_rfl , le_rfl ⟩
btw_cyclic_left { a b c } h := by
dsimp
rwa [ ← or_assoc : ∀ {a b c : Prop }, (a ∨ b ∨ c ↔ a ∨ b ∨ c , or_comm : ∀ {a b : Prop }, a ∨ b ↔ b ∨ a ]
sbtw_trans_left { a b c d } := by
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) : sbtw a b c ⟨hab, hbc⟩ : a < b ∧ b < c hab ⟨hab, hbc⟩ : a < b ∧ b < c hbc ⟨hab, hbc⟩ : a < b ∧ b < c ⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩ : sbtw a b c ⟨hbc, hca⟩ : b < c ∧ c < a hbc ⟨hbc, hca⟩ : b < c ∧ c < a hca ⟨hbc, hca⟩ : b < c ∧ c < a ⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩ : sbtw a b c ⟨hca, hab⟩ : c < a ∧ a < b hca ⟨hca, hab⟩ : c < a ∧ a < b hab ⟨hca, hab⟩ : c < a ∧ a < b (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) : sbtw a b c (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩) : sbtw b d c ⟨hbd, hdc⟩ : b < d ∧ d < c hbd ⟨hbd, hdc⟩ : b < d ∧ d < c hdc ⟨hbd, hdc⟩ : b < d ∧ d < c ⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩ : d < c ∧ c < b ∨ c < b ∧ b < d ⟨hdc, hcb⟩ : d < c ∧ c < b hdc ⟨hdc, hcb⟩ : d < c ∧ c < b hcb ⟨hdc, hcb⟩ : d < c ∧ c < b ⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩ : d < c ∧ c < b ∨ c < b ∧ b < d ⟨hcb, hbd⟩ : c < b ∧ b < d hcb ⟨hcb, hbd⟩ : c < b ∧ b < d hbd ⟨hcb, hbd⟩ : c < b ∧ b < d (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩) : sbtw b d c α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hbd : b < d hdc : d < c inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hdc : d < c hcb : c < b inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hcb : c < b hbd : b < d inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hbd : b < d hdc : d < c inr.inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hbd : b < d hdc : d < c inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hbd : b < d hdc : d < c inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hdc : d < c hcb : c < b inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hcb : c < b hbd : b < d inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hbd : b < d hdc : d < c inr.inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ hab . trans : ∀ {α : Type ?u.239719} [inst : Preorder α a b c : α }, a < b b < c a < c hbd , hdc ⟩
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hdc : d < c hcb : c < b inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hdc : d < c hcb : c < b inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hcb : c < b hbd : b < d inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hbd : b < d hdc : d < c inr.inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact ( hbc . not_lt : ∀ {α : Type ?u.239736} [inst : Preorder α a b : α }, a < b ¬ b < a hcb ). elim
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hcb : c < b hbd : b < d inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hab : a < b hbc : b < c hcb : c < b hbd : b < d inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hbd : b < d hdc : d < c inr.inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact ( hbc . not_lt : ∀ {α : Type ?u.239751} [inst : Preorder α a b : α }, a < b ¬ b < a hcb ). elim
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hbd : b < d hdc : d < c inr.inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hbd : b < d hdc : d < c inr.inl.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ hdc , hca ⟩)
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hdc : d < c hcb : c < b inr.inl.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ hdc , hca ⟩)
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hbc : b < c hca : c < a hcb : c < b hbd : b < d inr.inl.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact ( hbc . not_lt : ∀ {α : Type ?u.239786} [inst : Preorder α a b : α }, a < b ¬ b < a hcb ). elim
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hbd : b < d hdc : d < c inr.inr.intro.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ hdc , hca ⟩)
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hdc : d < c hcb : c < b inr.inr.intro.inr.inl.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b ⟨ hdc , hca ⟩)
· α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro α : Type ?u.3964inst✝ : Preorder α a, b, c, d : α hca : c < a hab : a < b hcb : c < b hbd : b < d inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inr : ∀ {a b : Prop }, b → a ∨ b ⟨ hca , hab . trans : ∀ {α : Type ?u.239831} [inst : Preorder α a b c : α }, a < b b < c a < c hbd ⟩)
sbtw_iff_btw_not_btw { a b c } := by
simp_rw [ lt_iff_le_not_le ]
have := le_trans : ∀ {α : Type ?u.4361} [self : Preorder α a b c : α ), a ≤ b b ≤ c a ≤ c a b c
have := le_trans : ∀ {α : Type ?u.4381} [self : Preorder α a b c : α ), a ≤ b b ≤ c a ≤ c b c a α : Type ?u.3964inst✝ : Preorder α a, b, c : α this✝ : a ≤ b b ≤ c a ≤ c this : b ≤ c c ≤ a b ≤ a
have := le_trans : ∀ {α : Type ?u.4400} [self : Preorder α a b c : α ), a ≤ b b ≤ c a ≤ c c a b α : Type ?u.3964inst✝ : Preorder α a, b, c : α this✝¹ : a ≤ b b ≤ c a ≤ c this✝ : b ≤ c c ≤ a b ≤ a this : c ≤ a a ≤ b c ≤ b
tauto
#align preorder.to_circular_preorder Preorder.toCircularPreorder
/-- The circular partial order obtained from "looping around" a partial order.
See note [reducible non-instances]. -/
@[reducible]
def PartialOrder.toCircularPartialOrder ( α : Type _ : Type (?u.241064+1)) [ PartialOrder : Type ?u.241067 → Type ?u.241067 α ] : CircularPartialOrder : Type ?u.241070 → Type ?u.241070 α :=
{ Preorder.toCircularPreorder α with
btw_antisymm := fun { a b c } => by
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) : btw a b c ⟨hab, hbc⟩ : a ≤ b ∧ b ≤ c hab ⟨hab, hbc⟩ : a ≤ b ∧ b ≤ c hbc ⟨hab, hbc⟩ : a ≤ b ∧ b ≤ c ⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩ : btw a b c ⟨hbc, hca⟩ : b ≤ c ∧ c ≤ a hbc ⟨hbc, hca⟩ : b ≤ c ∧ c ≤ a hca ⟨hbc, hca⟩ : b ≤ c ∧ c ≤ a ⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩ : btw a b c ⟨hca, hab⟩ : c ≤ a ∧ a ≤ b hca ⟨hca, hab⟩ : c ≤ a ∧ a ≤ b hab ⟨hca, hab⟩ : c ≤ a ∧ a ≤ b (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) : btw a b c (⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩) : btw c b a ⟨hcb, hba⟩ : c ≤ b ∧ b ≤ a hcb ⟨hcb, hba⟩ : c ≤ b ∧ b ≤ a hba ⟨hcb, hba⟩ : c ≤ b ∧ b ≤ a ⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩ : btw c b a ⟨hba, hac⟩ : b ≤ a ∧ a ≤ c hba ⟨hba, hac⟩ : b ≤ a ∧ a ≤ c hac ⟨hba, hac⟩ : b ≤ a ∧ a ≤ c ⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩ : btw c b a ⟨hac, hcb⟩ : a ≤ c ∧ c ≤ b hac ⟨hac, hcb⟩ : a ≤ c ∧ c ≤ b hcb ⟨hac, hcb⟩ : a ≤ c ∧ c ≤ b (⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩) : btw c b a inl.intro.inl.intro inl.intro.inr.inl.intro inl.intro.inr.inr.intro inr.inl.intro.inl.intro inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro
· inl.intro.inl.intro inl.intro.inr.inl.intro inl.intro.inr.inr.intro inr.inl.intro.inl.intro inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inl : ∀ {a b : Prop }, a → a ∨ b ( hab . antisymm hba )
· inl.intro.inr.inl.intro inl.intro.inr.inr.intro inr.inl.intro.inl.intro inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inl : ∀ {a b : Prop }, a → a ∨ b ( hab . antisymm hba )
· inl.intro.inr.inr.intro inr.inl.intro.inl.intro inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b <| hbc . antisymm hcb )
· inr.inl.intro.inl.intro inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b <| hbc . antisymm hcb )
· inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inl.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inr : ∀ {a b : Prop }, b → a ∨ b <| hca . antisymm hac )
· inr.inl.intro.inr.inr.intro inr.inl.intro.inr.inr.intro inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inr : ∀ {a b : Prop }, b → a ∨ b ( Or.inl : ∀ {a b : Prop }, a → a ∨ b <| hbc . antisymm hcb )
· inr.inr.intro.inl.intro inr.inr.intro.inr.inl.intro inr.inr.intro.inr.inr.intro exact Or.inl : ∀ {a b : Prop }, a → a ∨ b (