Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-11 21:25 788240cf

View on Github →

chore(order/cover): Rename covers to covby (#11984) This matches the way it is written. a ⋖ b means that b covers a, that is a is covered by b.

Estimated changes

added theorem bot_covby_iff
added theorem bot_covby_top
deleted theorem bot_covers_iff
deleted theorem bot_covers_top
added theorem covby_top_iff
deleted theorem covers_top_iff
added theorem apply_covby_apply_iff
deleted theorem apply_covers_apply_iff
added theorem covby.Icc_eq
added theorem covby.Ico_eq
added theorem covby.Ioc_eq
added theorem covby.Ioo_eq
added theorem covby.image
added theorem covby.le
added theorem covby.lt
added theorem covby.ne'
added theorem covby.of_image
added def covby
deleted theorem covers.Icc_eq
deleted theorem covers.Ico_eq
deleted theorem covers.Ioc_eq
deleted theorem covers.Ioo_eq
deleted theorem covers.image
deleted theorem covers.le
deleted theorem covers.lt
deleted theorem covers.ne'
deleted theorem covers.of_image
deleted def covers
added theorem not_covby
added theorem not_covby_iff
deleted theorem not_covers
deleted theorem not_covers_iff
added theorem covby.pred_eq
added theorem covby.succ_eq
added theorem covby_iff_pred_eq
added theorem covby_iff_succ_eq
deleted theorem covers.pred_eq
deleted theorem covers.succ_eq
deleted theorem covers_iff_pred_eq
deleted theorem covers_iff_succ_eq
added theorem pred_order.pred_covby
deleted theorem pred_order.pred_covers
modified theorem pred_succ
added theorem succ_order.covby_succ
deleted theorem succ_order.covers_succ
modified theorem succ_pred