Commit 2024-01-09 09:25 8b47b2fc

View on Github →

chore(Covby): rename Covby to CovBy (#9578) Rename

  • Covby → CovBy, Wcovby → WCovBy
  • *covby* → *covBy*
  • wcovby.finset_val → WCovBy.finset_val, wcovby.finset_coe → WCovBy.finset_coe
  • Covby.is_coatom → CovBy.isCoatom

Estimated changes

deleted theorem toIocDiv_wcovby_toIcoDiv
modified theorem Flag.mem_rangeFin
added theorem CovBy.card_finset
added theorem CovBy.card_multiset
deleted theorem Covby.card_finset
deleted theorem Covby.card_multiset
deleted theorem Covby.exists_finset_cons
deleted theorem Covby.exists_finset_erase
added theorem Finset.coe_covBy_coe
deleted theorem Finset.coe_covby_coe
added theorem Finset.coe_wcovBy_coe
deleted theorem Finset.coe_wcovby_coe
added theorem Finset.covBy_cons
added theorem Finset.covBy_insert
deleted theorem Finset.covby_cons
deleted theorem Finset.covby_insert
added theorem Finset.erase_covBy
deleted theorem Finset.erase_covby
added theorem Finset.erase_wcovBy
deleted theorem Finset.erase_wcovby
added theorem Finset.val_covBy_val
deleted theorem Finset.val_covby_val
added theorem Finset.val_wcovBy_val
deleted theorem Finset.val_wcovby_val
added theorem Finset.wcovBy_insert
deleted theorem Finset.wcovby_insert
added theorem Multiset.covBy_cons
added theorem Multiset.covBy_iff
deleted theorem Multiset.covby_cons
deleted theorem Multiset.covby_iff
modified theorem Multiset.isAtom_iff
deleted theorem antitone_iff_forall_covby
deleted theorem le_iff_reflTransGen_covby
added theorem le_iff_transGen_wcovBy
deleted theorem le_iff_transGen_wcovby
added theorem lt_iff_transGen_covBy
deleted theorem lt_iff_transGen_covby
deleted theorem monotone_iff_forall_covby
added theorem transGen_covBy_of_lt
deleted theorem transGen_covby_of_lt
added theorem transGen_wcovBy_of_le
deleted theorem transGen_wcovby_of_le
added theorem Int.covBy_add_one
deleted theorem Int.covby_add_one
added theorem Int.sub_one_covBy
deleted theorem Int.sub_one_covby
added theorem Nat.cast_int_covBy_iff
deleted theorem Nat.cast_int_covby_iff
added theorem Fin.coe_covBy_iff
deleted theorem Fin.coe_covby_iff
added theorem Basis.flag_covBy
deleted theorem Basis.flag_covby
added theorem Basis.flag_wcovBy
deleted theorem Basis.flag_wcovby
added theorem bot_covBy_iff
added theorem bot_covBy_top
deleted theorem bot_covby_iff
deleted theorem bot_covby_top
added theorem covBy_iff_atom_Ici
added theorem covBy_iff_coatom_Iic
added theorem covBy_top_iff
deleted theorem covby_iff_atom_Ici
deleted theorem covby_iff_coatom_Iic
deleted theorem covby_top_iff
deleted theorem AntisymmRel.trans_covby
deleted theorem AntisymmRel.trans_wcovby
added theorem AntisymmRel.wcovBy
deleted 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.of_le_of_lt
added theorem CovBy.of_lt_of_le
added theorem CovBy.unique_left
added theorem CovBy.unique_right
added def CovBy
deleted theorem Covby.Icc_eq
deleted theorem Covby.Ico_eq
deleted theorem Covby.Iio_eq
deleted theorem Covby.Ioc_eq
deleted theorem Covby.Ioi_eq
deleted theorem Covby.Ioo_eq
deleted theorem Covby.eq_of_between
deleted theorem Covby.eq_or_eq
deleted theorem Covby.exists_set_insert
deleted theorem Covby.ge_of_gt
deleted theorem Covby.image
deleted theorem Covby.le
deleted theorem Covby.le_of_lt
deleted theorem Covby.lt
deleted theorem Covby.ne'
deleted theorem Covby.of_image
deleted theorem Covby.of_le_of_lt
deleted theorem Covby.of_lt_of_le
deleted theorem Covby.trans_antisymmRel
deleted theorem Covby.unique_left
deleted theorem Covby.unique_right
deleted def Covby
added theorem Prod.covBy_iff
deleted theorem Prod.covby_iff
added theorem Prod.mk_covBy_mk_iff
deleted theorem Prod.mk_covby_mk_iff
deleted theorem Prod.mk_covby_mk_iff_left
added theorem Prod.mk_wcovBy_mk_iff
deleted theorem Prod.mk_wcovby_mk_iff
added theorem Prod.swap_covBy_swap
deleted theorem Prod.swap_covby_swap
added theorem Prod.swap_wcovBy_swap
deleted theorem Prod.swap_wcovby_swap
added theorem Prod.wcovBy_iff
deleted theorem Prod.wcovby_iff
added theorem Set.covBy_insert
deleted theorem Set.covby_insert
deleted theorem Set.sdiff_singleton_covby
added theorem Set.wcovBy_insert
deleted 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.of_le_of_le'
added theorem WCovBy.of_le_of_le
added theorem WCovBy.refl
added theorem WCovBy.rfl
added theorem WCovBy.snd
added theorem WCovBy.sup_eq
added theorem WCovBy.wcovBy_iff_le
added def WCovBy
deleted theorem Wcovby.Icc_eq
deleted theorem Wcovby.Ico_subset
deleted theorem Wcovby.Ioc_subset
deleted theorem Wcovby.Ioo_eq
deleted theorem Wcovby.covby_of_lt
deleted theorem Wcovby.covby_of_ne
deleted theorem Wcovby.covby_of_not_le
deleted theorem Wcovby.eq_or_eq
deleted theorem Wcovby.fst
deleted theorem Wcovby.ge_of_gt
deleted theorem Wcovby.image
deleted theorem Wcovby.inf_eq
deleted theorem Wcovby.le
deleted theorem Wcovby.le_and_le_iff
deleted theorem Wcovby.le_of_lt
deleted theorem Wcovby.of_image
deleted theorem Wcovby.of_le_of_le'
deleted theorem Wcovby.of_le_of_le
deleted theorem Wcovby.refl
deleted theorem Wcovby.rfl
deleted theorem Wcovby.snd
deleted theorem Wcovby.sup_eq
deleted theorem Wcovby.trans_antisymm_rel
deleted theorem Wcovby.wcovby_iff_le
deleted def Wcovby
added theorem apply_covBy_apply_iff
deleted theorem apply_covby_apply_iff
added theorem apply_wcovBy_apply_iff
deleted theorem apply_wcovby_apply_iff
added theorem covBy_congr_left
added theorem covBy_congr_right
added theorem covBy_iff_Ioo_eq
added theorem covBy_of_eq_or_eq
deleted theorem covby_congr_left
deleted theorem covby_congr_right
deleted theorem covby_iff_Ioo_eq
deleted theorem covby_iff_lt_and_eq_or_eq
deleted theorem covby_iff_wcovby_and_lt
deleted theorem covby_iff_wcovby_and_ne
deleted theorem covby_of_eq_or_eq
added theorem not_covBy
added theorem not_covBy_iff
added theorem not_covBy_of_lt_of_lt
deleted theorem not_covby
deleted theorem not_covby_iff
deleted theorem not_covby_of_lt_of_lt
added theorem not_wcovBy_iff
deleted theorem not_wcovby_iff
deleted theorem ofDual_covby_ofDual_iff
deleted theorem ofDual_wcovby_ofDual_iff
deleted theorem toDual_covby_toDual_iff
deleted 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_eq_or_covBy
added theorem wcovBy_of_eq_or_eq
added theorem wcovBy_of_le_of_le
deleted theorem wcovby_congr_left
deleted theorem wcovby_congr_right
deleted theorem wcovby_eq_reflGen_covby
deleted theorem wcovby_iff_Ioo_eq
deleted theorem wcovby_iff_covby_or_eq
deleted theorem wcovby_iff_eq_or_covby
deleted theorem wcovby_of_eq_or_eq
deleted theorem wcovby_of_le_of_le
deleted theorem covby_iff_lt_covby_grade
added theorem grade_covBy_grade_iff
deleted theorem grade_covby_grade_iff
added theorem CovBy.pred_eq
added theorem CovBy.succ_eq
deleted theorem Covby.pred_eq
deleted theorem Covby.succ_eq
added theorem Order.covBy_succ
deleted theorem Order.covby_succ
added theorem Order.pred_covBy
deleted theorem Order.pred_covby
deleted theorem Order.pred_eq_iff_covby
added theorem Order.pred_wcovBy
deleted theorem Order.pred_wcovby
deleted theorem Order.succ_eq_iff_covby
added theorem Order.wcovBy_succ
deleted theorem Order.wcovby_succ
added theorem WCovBy.le_succ
added theorem WCovBy.pred_le
deleted theorem Wcovby.le_succ
deleted theorem Wcovby.pred_le
modified theorem Order.isPredLimit_of_dense
modified theorem Order.isSuccLimit_of_dense
deleted theorem covby_iff_quot_is_simple
modified theorem Ordinal.nhds_right'
added theorem CovBy.nhdsWithin_Iio
added theorem CovBy.nhdsWithin_Ioi
deleted theorem Covby.nhdsWithin_Iio
deleted theorem Covby.nhdsWithin_Ioi