Commit 2023-01-12 06:33 90a54f41

View on Github →

feat: port Order.Circular (#1489)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Circular.lean

added theorem Btw.btw.antisymm

added theorem Btw.btw.cyclic_left

added def LE.toBtw

added def LT.toSBtw

added def LinearOrder.toCircularOrder

added def PartialOrder.toCircularPartialOrder

added def Preorder.toCircularPreorder

added theorem SBtw.sbtw.trans_left

added def Set.cIcc

added def Set.cIoo

added theorem Set.compl_cIcc

added theorem Set.compl_cIoo

added theorem Set.left_mem_cIcc

added theorem Set.mem_cIcc

added theorem Set.mem_cIoo

added theorem Set.right_mem_cIcc

added theorem btw_cyclic

added theorem btw_cyclic_right

added theorem btw_iff_not_sbtw

added theorem btw_of_sbtw

added theorem btw_refl_left

added theorem btw_refl_left_right

added theorem btw_refl_right

added theorem btw_rfl

added theorem btw_rfl_left

added theorem btw_rfl_left_right

added theorem btw_rfl_right

added theorem not_btw_of_sbtw

added theorem not_sbtw_of_btw

added theorem sbtw_asymm

added theorem sbtw_cyclic

added theorem sbtw_cyclic_left

added theorem sbtw_cyclic_right

added theorem sbtw_iff_btw_not_btw

added theorem sbtw_iff_not_btw

added theorem sbtw_irrefl

added theorem sbtw_irrefl_left

added theorem sbtw_irrefl_left_right

added theorem sbtw_irrefl_right

added theorem sbtw_of_btw_not_btw

added theorem sbtw_trans_right