Commit 2022-12-26 20:25 26b1d769

View on Github →

feat: port Order.Cover (#1200)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Cover.lean

added theorem AntisymmRel.trans_covby

added theorem AntisymmRel.trans_wcovby

added theorem AntisymmRel.wcovby

added theorem Covby.Icc_eq

added theorem Covby.Ico_eq

added theorem Covby.Iio_eq

added theorem Covby.Ioc_eq

added theorem Covby.Ioi_eq

added theorem Covby.Ioo_eq

added theorem Covby.eq_of_between

added theorem Covby.eq_or_eq

added theorem Covby.ge_of_gt

added theorem Covby.image

added theorem Covby.le

added theorem Covby.le_of_lt

added theorem Covby.lt

added theorem Covby.ne'

added theorem Covby.of_image

added theorem Covby.trans_antisymmRel

added theorem Covby.unique_left

added theorem Covby.unique_right

added def Covby

added theorem Prod.covby_iff

added theorem Prod.fst_eq_or_snd_eq_of_wcovby

added theorem Prod.mk_covby_mk_iff

added theorem Prod.mk_covby_mk_iff_left

added theorem Prod.mk_covby_mk_iff_right

added theorem Prod.mk_wcovby_mk_iff

added theorem Prod.mk_wcovby_mk_iff_left

added theorem Prod.mk_wcovby_mk_iff_right

added theorem Prod.swap_covby_swap

added theorem Prod.swap_wcovby_swap

added theorem Prod.wcovby_iff

added theorem Set.OrdConnected.apply_covby_apply_iff

added theorem Set.OrdConnected.apply_wcovby_apply_iff

added theorem Set.covby_insert

added theorem Set.wcovby_insert

added theorem Wcovby.Icc_eq

added theorem Wcovby.Ico_subset

added theorem Wcovby.Ioc_subset

added theorem Wcovby.Ioo_eq

added theorem Wcovby.covby_of_lt

added theorem Wcovby.covby_of_ne

added theorem Wcovby.covby_of_not_le

added theorem Wcovby.eq_or_eq

added theorem Wcovby.fst

added theorem Wcovby.ge_of_gt

added theorem Wcovby.image

added theorem Wcovby.inf_eq

added theorem Wcovby.le

added theorem Wcovby.le_and_le_iff

added theorem Wcovby.le_of_lt

added theorem Wcovby.of_image

added theorem Wcovby.refl

added theorem Wcovby.rfl

added theorem Wcovby.snd

added theorem Wcovby.sup_eq

added theorem Wcovby.trans_antisymm_rel

added theorem Wcovby.wcovby_iff_le

added def Wcovby

added theorem apply_covby_apply_iff

added theorem apply_wcovby_apply_iff

added theorem covby_congr_left

added theorem covby_congr_right

added theorem covby_iff_Ioo_eq

added theorem covby_iff_lt_and_eq_or_eq

added theorem covby_iff_wcovby_and_lt

added theorem covby_iff_wcovby_and_ne

added theorem covby_iff_wcovby_and_not_le

added theorem covby_of_eq_or_eq

added theorem densely_ordered_iff_forall_not_covby

added theorem not_covby

added theorem not_covby_iff

added theorem not_covby_of_lt_of_lt

added theorem not_wcovby_iff

added theorem ofDual_covby_ofDual_iff

added theorem ofDual_wcovby_ofDual_iff

added theorem toDual_covby_toDual_iff

added theorem toDual_wcovby_toDual_iff

added theorem wcovby_congr_left

added theorem wcovby_congr_right

added theorem wcovby_iff_Ioo_eq

added theorem wcovby_iff_covby_or_eq

added theorem wcovby_iff_covby_or_le_and_le

added theorem wcovby_iff_eq_or_covby

added theorem wcovby_iff_le_and_eq_or_eq

added theorem wcovby_of_eq_or_eq

added theorem wcovby_of_le_of_le