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	24 math math: Set.mem_cIcc, btw_of_sbtw, sbtw_iff_btw_not_btw, not_btw_of_sbtw, btw_refl_left, btw_rfl_left_right, btw_iff_not_sbtw, CircularPreorder.btw_refl, QuotientAddGroup.btw_coe_iff, CircularOrder.btw_total, btw_rfl_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 📖	—	Btw.btw CircularPreorder.toBtw	—	—	CircularPreorder.btw_cyclic_left
cyclic_right 📖	—	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	21 math math: Set.mem_cIcc, btw_of_sbtw, sbtw_iff_btw_not_btw, not_btw_of_sbtw, btw_refl_left, btw_rfl_left_right, btw_iff_not_sbtw, btw_refl, CircularOrder.btw_total, btw_rfl_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	16 math math: sbtw_irrefl_right, not_sbtw_of_btw, sbtw_iff_btw_not_btw, sbtw_cyclic, Fin.sbtw_iff, btw_iff_not_sbtw, sbtw_irrefl_left_right, sbtw_of_btw_not_btw, sbtw_irrefl, Set.mem_cIoo, Btw.btw.sbtw_of_not_btw, sbtw_iff_btw_not_btw, sbtw_irrefl_left, Btw.btw.not_sbtw, sbtw_iff_not_btw, Int.sbtw_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
btw_cyclic_left 📖	—	Btw.btw toBtw	—	—	—
btw_refl 📖	mathematical	—	Btw.btw toBtw	—	—
sbtw_iff_btw_not_btw 📖	mathematical	—	SBtw.sbtw toSBtw Btw.btw toBtw	—	—
sbtw_trans_left 📖	—	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	17 math math: sbtw_irrefl_right, not_sbtw_of_btw, sbtw_iff_btw_not_btw, sbtw_cyclic, Fin.sbtw_iff, btw_iff_not_sbtw, sbtw_irrefl_left_right, sbtw_iff, sbtw_of_btw_not_btw, sbtw_irrefl, Set.mem_cIoo, Btw.btw.sbtw_of_not_btw, CircularPreorder.sbtw_iff_btw_not_btw, sbtw_irrefl_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 📖	—	SBtw.sbtw CircularPreorder.toSBtw	—	—	sbtw_cyclic_left
cyclic_right 📖	—	SBtw.sbtw CircularPreorder.toSBtw	—	—	sbtw_cyclic_right
not_btw 📖	mathematical	SBtw.sbtw CircularPreorder.toSBtw	Btw.btw CircularPreorder.toBtw	—	not_btw_of_sbtw
not_sbtw 📖	—	SBtw.sbtw CircularPreorder.toSBtw	—	—	sbtw_asymm
trans_left 📖	—	SBtw.sbtw CircularPreorder.toSBtw	—	—	CircularPreorder.sbtw_trans_left
trans_right 📖	—	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 📖	—	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 📖	—	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 📖	—	SBtw.sbtw CircularPreorder.toSBtw	—	—	Btw.btw.sbtw_of_not_btw Btw.btw.cyclic_left SBtw.sbtw.btw SBtw.sbtw.not_btw
sbtw_cyclic_right 📖	—	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 📖	—	SBtw.sbtw CircularPreorder.toSBtw	—	—	SBtw.sbtw.cyclic_right SBtw.sbtw.trans_left SBtw.sbtw.cyclic_left

---

← Back to Index