Commit 2021-10-01 20:36 05ee42cf

View on Github →

feat(order/circular): define circular orders (#9413) A circular order is the way to formalize positions on a circle. This is very foundational, as a good lot of the order-algebra-topology hierarchy has a circular analog.

Estimated changes

Created src/order/circular.lean

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 has_btw.btw.antisymm

added theorem has_btw.btw.cyclic_left

added def has_le.to_has_btw

added def has_lt.to_has_sbtw

added theorem has_sbtw.sbtw.trans_left

added def linear_order.to_circular_order

added theorem not_btw_of_sbtw

added theorem not_sbtw_of_btw

added def partial_order.to_circular_partial_order

added def preorder.to_circular_preorder

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

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