Circular

📁 Source: Mathlib/Order/Circular.lean

Statistics

Metric	Count
Definitions `Btw`, `btw`, `CircularOrder`, `toCircularPartialOrder`, `CircularPartialOrder`, `toCircularPreorder`, `CircularPreorder`, `toBtw`, `toSBtw`, `toBtw`, `toSBtw`, `toCircularOrder`, `btw`, `circularPartialOrder`, `circularPreorder`, `instCircularOrder`, `sbtw`, `toCircularPartialOrder`, `toCircularPreorder`, `SBtw`, `sbtw`, `cIcc`, `cIoo`	23
Theorems `antisymm`, `cyclic_left`, `cyclic_right`, `not_sbtw`, `sbtw_of_not_btw`, `btw_total`, `btw_antisymm`, `btw_cyclic_left`, `btw_refl`, `sbtw_iff_btw_not_btw`, `sbtw_trans_left`, `btw`, `cyclic_left`, `cyclic_right`, `not_btw`, `not_sbtw`, `trans_left`, `trans_right`, `compl_cIcc`, `compl_cIoo`, `left_mem_cIcc`, `mem_cIcc`, `mem_cIoo`, `right_mem_cIcc`, `btw_cyclic`, `btw_cyclic_right`, `btw_iff`, `btw_iff_not_sbtw`, `btw_of_sbtw`, `btw_refl_left`, `btw_refl_left_right`, `btw_refl_right`, `btw_rfl`, `btw_rfl_left`, `btw_rfl_left_right`, `btw_rfl_right`, `not_btw_of_sbtw`, `not_sbtw_of_btw`, `sbtw_asymm`, `sbtw_cyclic`, `sbtw_cyclic_left`, `sbtw_cyclic_right`, `sbtw_iff`, `sbtw_iff_btw_not_btw`, `sbtw_iff_not_btw`, `sbtw_irrefl`, `sbtw_irrefl_left`, `sbtw_irrefl_left_right`, `sbtw_irrefl_right`, `sbtw_of_btw_not_btw`, `sbtw_trans_right`	51
Total	74

Btw

Definitions

Name	Category	Theorems
`btw` 📖	MathDef	28 math math: `Set.mem_cIcc`, `btw_of_sbtw`, `btw.cyclic_left`, `sbtw_iff_btw_not_btw`, `btw.cyclic_right`, `not_btw_of_sbtw`, `btw_refl_left`, `btw_rfl_left_right`, `btw_iff_not_sbtw`, `btw_cyclic_right`, `CircularPreorder.btw_refl`, `QuotientAddGroup.btw_coe_iff`, `CircularOrder.btw_total`, `btw_rfl_left`, `CircularPreorder.btw_cyclic_left`, `QuotientAddGroup.btw_coe_iff'`, `Fin.btw_iff`, `btw_rfl_right`, `btw_rfl`, `CircularPreorder.sbtw_iff_btw_not_btw`, `btw_iff`, `Int.btw_iff`, `btw_refl_left_right`, `btw_cyclic`, `sbtw_iff_not_btw`, `btw_refl_right`, `SBtw.sbtw.btw`, `SBtw.sbtw.not_btw`

Btw.btw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder`	—	—	`CircularPartialOrder.btw_antisymm`
`cyclic_left` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`CircularPreorder.btw_cyclic_left`
`cyclic_right` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`btw_cyclic_right`
`not_sbtw` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`not_sbtw_of_btw`
`sbtw_of_not_btw` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_of_btw_not_btw`

CircularOrder

Definitions

Name	Category	Theorems
`toCircularPartialOrder` 📖	CompOp	17 math math: `Set.compl_cIoo`, `Set.left_mem_cIcc`, `Fin.sbtw_iff`, `Set.compl_cIcc`, `btw_refl_left`, `btw_rfl_left_right`, `btw_iff_not_sbtw`, `btw_total`, `btw_rfl_left`, `Fin.btw_iff`, `btw_rfl_right`, `Set.right_mem_cIcc`, `Int.btw_iff`, `btw_refl_left_right`, `sbtw_iff_not_btw`, `btw_refl_right`, `Int.sbtw_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`btw_total` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `toCircularPartialOrder`	—	—

CircularPartialOrder

Definitions

Name	Category	Theorems
`toCircularPreorder` 📖	CompOp	17 math math: `Set.compl_cIoo`, `Set.left_mem_cIcc`, `Fin.sbtw_iff`, `Set.compl_cIcc`, `btw_refl_left`, `btw_rfl_left_right`, `btw_iff_not_sbtw`, `CircularOrder.btw_total`, `btw_rfl_left`, `Fin.btw_iff`, `btw_rfl_right`, `Set.right_mem_cIcc`, `Int.btw_iff`, `btw_refl_left_right`, `sbtw_iff_not_btw`, `btw_refl_right`, `Int.sbtw_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`btw_antisymm` 📖	—	`Btw.btw` `CircularPreorder.toBtw` `toCircularPreorder`	—	—	—

CircularPreorder

Definitions

Name	Category	Theorems
`toBtw` 📖	CompOp	25 math math: `Set.mem_cIcc`, `btw_of_sbtw`, `Btw.btw.cyclic_left`, `sbtw_iff_btw_not_btw`, `Btw.btw.cyclic_right`, `not_btw_of_sbtw`, `btw_refl_left`, `btw_rfl_left_right`, `btw_iff_not_sbtw`, `btw_cyclic_right`, `btw_refl`, `CircularOrder.btw_total`, `btw_rfl_left`, `btw_cyclic_left`, `Fin.btw_iff`, `btw_rfl_right`, `btw_rfl`, `sbtw_iff_btw_not_btw`, `Int.btw_iff`, `btw_refl_left_right`, `btw_cyclic`, `sbtw_iff_not_btw`, `btw_refl_right`, `SBtw.sbtw.btw`, `SBtw.sbtw.not_btw`
`toSBtw` 📖	CompOp	26 math math: `SBtw.sbtw.cyclic_left`, `sbtw_irrefl_right`, `sbtw_trans_left`, `not_sbtw_of_btw`, `SBtw.sbtw.not_sbtw`, `sbtw_iff_btw_not_btw`, `SBtw.sbtw.trans_right`, `sbtw_cyclic`, `Fin.sbtw_iff`, `sbtw_cyclic_left`, `sbtw_cyclic_right`, `btw_iff_not_sbtw`, `sbtw_irrefl_left_right`, `sbtw_trans_right`, `SBtw.sbtw.cyclic_right`, `sbtw_of_btw_not_btw`, `sbtw_irrefl`, `Set.mem_cIoo`, `Btw.btw.sbtw_of_not_btw`, `sbtw_asymm`, `sbtw_iff_btw_not_btw`, `sbtw_irrefl_left`, `SBtw.sbtw.trans_left`, `Btw.btw.not_sbtw`, `sbtw_iff_not_btw`, `Int.sbtw_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`btw_cyclic_left` 📖	mathematical	`Btw.btw` `toBtw`	`Btw.btw` `toBtw`	—	—
`btw_refl` 📖	mathematical	—	`Btw.btw` `toBtw`	—	—
`sbtw_iff_btw_not_btw` 📖	mathematical	—	`SBtw.sbtw` `toSBtw` `Btw.btw` `toBtw`	—	—
`sbtw_trans_left` 📖	mathematical	`SBtw.sbtw` `toSBtw`	`SBtw.sbtw` `toSBtw`	—	—

LE

Definitions

Name	Category	Theorems
`toBtw` 📖	CompOp	1 math math: `btw_iff`

LT

Definitions

Name	Category	Theorems
`toSBtw` 📖	CompOp	1 math math: `sbtw_iff`

LinearOrder

Definitions

Name	Category	Theorems
`toCircularOrder` 📖	CompOp	—

OrderDual

Definitions

Name	Category	Theorems
`btw` 📖	CompOp	—
`circularPartialOrder` 📖	CompOp	—
`circularPreorder` 📖	CompOp	—
`instCircularOrder` 📖	CompOp	—
`sbtw` 📖	CompOp	—

PartialOrder

Definitions

Name	Category	Theorems
`toCircularPartialOrder` 📖	CompOp	—

Preorder

Definitions

Name	Category	Theorems
`toCircularPreorder` 📖	CompOp	—

SBtw

Definitions

Name	Category	Theorems
`sbtw` 📖	MathDef	27 math math: `sbtw.cyclic_left`, `sbtw_irrefl_right`, `CircularPreorder.sbtw_trans_left`, `not_sbtw_of_btw`, `sbtw.not_sbtw`, `sbtw_iff_btw_not_btw`, `sbtw.trans_right`, `sbtw_cyclic`, `Fin.sbtw_iff`, `sbtw_cyclic_left`, `sbtw_cyclic_right`, `btw_iff_not_sbtw`, `sbtw_irrefl_left_right`, `sbtw_iff`, `sbtw_trans_right`, `sbtw.cyclic_right`, `sbtw_of_btw_not_btw`, `sbtw_irrefl`, `Set.mem_cIoo`, `Btw.btw.sbtw_of_not_btw`, `sbtw_asymm`, `CircularPreorder.sbtw_iff_btw_not_btw`, `sbtw_irrefl_left`, `sbtw.trans_left`, `Btw.btw.not_sbtw`, `sbtw_iff_not_btw`, `Int.sbtw_iff`

SBtw.sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`btw` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`btw_of_sbtw`
`cyclic_left` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_cyclic_left`
`cyclic_right` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_cyclic_right`
`not_btw` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`not_btw_of_sbtw`
`not_sbtw` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_asymm`
`trans_left` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`CircularPreorder.sbtw_trans_left`
`trans_right` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_trans_right`

Set

Definitions

Name	Category	Theorems
`cIcc` 📖	CompOp	5 math math: `mem_cIcc`, `compl_cIoo`, `left_mem_cIcc`, `compl_cIcc`, `right_mem_cIcc`
`cIoo` 📖	CompOp	3 math math: `compl_cIoo`, `compl_cIcc`, `mem_cIoo`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_cIcc` 📖	mathematical	—	`Compl.compl` `Set` `instCompl` `cIcc` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder` `cIoo`	—	`ext` `mem_cIoo` `sbtw_iff_not_btw` `cIcc.eq_1` `mem_compl_iff` `mem_setOf`
`compl_cIoo` 📖	mathematical	—	`Compl.compl` `Set` `instCompl` `cIoo` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder` `cIcc`	—	`ext` `mem_cIcc` `btw_iff_not_sbtw` `cIoo.eq_1` `mem_compl_iff` `mem_setOf`
`left_mem_cIcc` 📖	mathematical	—	`Set` `instMembership` `cIcc` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`btw_rfl_left`
`mem_cIcc` 📖	mathematical	—	`Set` `instMembership` `cIcc` `Btw.btw` `CircularPreorder.toBtw`	—	—
`mem_cIoo` 📖	mathematical	—	`Set` `instMembership` `cIoo` `SBtw.sbtw` `CircularPreorder.toSBtw`	—	—
`right_mem_cIcc` 📖	mathematical	—	`Set` `instMembership` `cIcc` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`btw_rfl_right`

(root)

Definitions

Name	Category	Theorems
`Btw` 📖	CompData	—
`CircularOrder` 📖	CompData	—
`CircularPartialOrder` 📖	CompData	—
`CircularPreorder` 📖	CompData	—
`SBtw` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`btw_cyclic` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw`	—	`btw_cyclic_right` `CircularPreorder.btw_cyclic_left`
`btw_cyclic_right` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`Btw.btw.cyclic_left`
`btw_iff` 📖	mathematical	—	`Btw.btw` `LE.toBtw`	—	—
`btw_iff_not_sbtw` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder` `SBtw.sbtw` `CircularPreorder.toSBtw`	—	`iff_not_comm` `sbtw_iff_not_btw`
`btw_of_sbtw` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`sbtw_iff_btw_not_btw`
`btw_refl_left` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`Btw.btw.cyclic_right` `btw_rfl_left_right`
`btw_refl_left_right` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`CircularOrder.btw_total`
`btw_refl_right` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`Btw.btw.cyclic_left` `btw_rfl_left_right`
`btw_rfl` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw`	—	`CircularPreorder.btw_refl`
`btw_rfl_left` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`btw_refl_left`
`btw_rfl_left_right` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`btw_refl_left_right`
`btw_rfl_right` 📖	mathematical	—	`Btw.btw` `CircularPreorder.toBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder`	—	`btw_refl_right`
`not_btw_of_sbtw` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`Btw.btw` `CircularPreorder.toBtw`	—	`sbtw_iff_btw_not_btw`
`not_sbtw_of_btw` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`SBtw.sbtw.not_btw`
`sbtw_asymm` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`Btw.btw.not_sbtw` `SBtw.sbtw.btw`
`sbtw_cyclic` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_cyclic_right` `sbtw_cyclic_left`
`sbtw_cyclic_left` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`Btw.btw.sbtw_of_not_btw` `Btw.btw.cyclic_left` `SBtw.sbtw.btw` `SBtw.sbtw.not_btw`
`sbtw_cyclic_right` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`SBtw.sbtw.cyclic_left`
`sbtw_iff` 📖	mathematical	—	`SBtw.sbtw` `LT.toSBtw`	—	—
`sbtw_iff_btw_not_btw` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw` `Btw.btw` `CircularPreorder.toBtw`	—	`CircularPreorder.sbtw_iff_btw_not_btw`
`sbtw_iff_not_btw` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw` `CircularPartialOrder.toCircularPreorder` `CircularOrder.toCircularPartialOrder` `Btw.btw` `CircularPreorder.toBtw`	—	`sbtw_iff_btw_not_btw` `CircularOrder.btw_total`
`sbtw_irrefl` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_irrefl_left_right`
`sbtw_irrefl_left` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_irrefl_left_right` `SBtw.sbtw.cyclic_left`
`sbtw_irrefl_left_right` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`SBtw.sbtw.not_btw` `SBtw.sbtw.btw`
`sbtw_irrefl_right` 📖	mathematical	—	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_irrefl_left_right` `SBtw.sbtw.cyclic_right`
`sbtw_of_btw_not_btw` 📖	mathematical	`Btw.btw` `CircularPreorder.toBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`sbtw_iff_btw_not_btw`
`sbtw_trans_right` 📖	mathematical	`SBtw.sbtw` `CircularPreorder.toSBtw`	`SBtw.sbtw` `CircularPreorder.toSBtw`	—	`SBtw.sbtw.cyclic_right` `SBtw.sbtw.trans_left` `SBtw.sbtw.cyclic_left`

---

← Back to Index