Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 18:09 fec084c3

View on Github →

feat(order/cover): The covering relation (#10676) This defines a ⋖ b to mean that a < b and there is no element in between. It is generally useful, but in particular in the context of polytopes and successor orders.

Estimated changes

added theorem bot_covers_iff
added theorem bot_covers_top
added theorem covers_top_iff
modified theorem eq_bot_or_eq_of_le_atom
modified theorem eq_top_or_eq_of_coatom_le
modified theorem is_atom.Iic
modified theorem is_atom.of_is_atom_coe_Iic
modified theorem is_coatom.Ici
added theorem eq_of_ge_of_not_gt
added theorem eq_of_le_of_not_lt
added theorem covers.Icc_eq
added theorem covers.Ico_eq
added theorem covers.Ioc_eq
added theorem covers.Ioo_eq
added theorem covers.le
added theorem covers.lt
added theorem covers.ne'
added def covers
added theorem not_covers
added theorem not_covers_iff
added theorem covers.pred_eq
added theorem covers.succ_eq
added theorem covers_iff_pred_eq
added theorem covers_iff_succ_eq
added theorem pred_order.pred_covers
added theorem pred_succ
added theorem succ_order.covers_succ
added theorem succ_pred