Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 18:09 2c4e66f7

View on Github →

split(data/finset/*): Split data.finset.card and data.finset.fin off data.finset.basic (#10796) This moves stuff from data.finset.basic in two new files:

  • Stuff about finset.card goes into data.finset.card
  • Stuff about finset.fin_range and finset.attach_fin goes into data.finset.fin. I expect this file to be shortlived as I'm planning on killing fin_range. I reordered lemmas thematically and it appeared that there were two pairs of duplicated lemmas:
  • finset.one_lt_card, finset.one_lt_card_iff. They differ only for binder order.
  • finset.card_union_eq, finset.card_disjoint_union. They are literally the same. All are used so I will clean up in a later PR. I'm crediting:
  • Microsoft Corporation, Leonardo, Jeremy for 8dbee5b1ca9680a22ffe90751654f51d6852d7f0
  • Chris Hughes for #231
  • Scott for #3319

Estimated changes

deleted def finset.attach_fin
deleted def finset.card
deleted theorem finset.card_attach
deleted theorem finset.card_attach_fin
deleted theorem finset.card_congr
deleted theorem finset.card_cons
deleted theorem finset.card_def
deleted theorem finset.card_empty
deleted theorem finset.card_eq_one
deleted theorem finset.card_eq_succ
deleted theorem finset.card_eq_three
deleted theorem finset.card_eq_two
deleted theorem finset.card_eq_zero
deleted theorem finset.card_erase_eq_ite
deleted theorem finset.card_erase_le
deleted theorem finset.card_erase_of_mem
deleted theorem finset.card_filter_le
deleted theorem finset.card_image_le
deleted theorem finset.card_insert_eq_ite
deleted theorem finset.card_insert_le
deleted theorem finset.card_insert_of_mem
deleted theorem finset.card_le_of_subset
deleted theorem finset.card_le_one
deleted theorem finset.card_le_one_iff
deleted theorem finset.card_lt_card
deleted theorem finset.card_map
deleted theorem finset.card_mk
deleted theorem finset.card_mono
deleted theorem finset.card_pos
deleted theorem finset.card_range
deleted theorem finset.card_sdiff
deleted theorem finset.card_singleton
deleted theorem finset.card_subtype
deleted theorem finset.card_union_eq
deleted theorem finset.card_union_le
deleted theorem finset.coe_fin_range
deleted theorem finset.exists_smaller_set
deleted theorem finset.filter_card_eq
deleted def finset.fin_range
deleted theorem finset.fin_range_card
deleted theorem finset.length_to_list
deleted theorem finset.lt_wf
deleted theorem finset.mem_attach_fin
deleted theorem finset.mem_fin_range
deleted theorem finset.one_lt_card
deleted theorem finset.one_lt_card_iff
deleted theorem list.card_to_finset
deleted theorem list.to_finset_card_le
modified theorem multiset.to_finset_map
added def finset.card
added theorem finset.card_attach
added theorem finset.card_congr
added theorem finset.card_cons
added theorem finset.card_def
added theorem finset.card_empty
added theorem finset.card_eq_one
added theorem finset.card_eq_succ
added theorem finset.card_eq_three
added theorem finset.card_eq_two
added theorem finset.card_eq_zero
added theorem finset.card_erase_le
added theorem finset.card_filter_le
added theorem finset.card_image_le
added theorem finset.card_insert_le
added theorem finset.card_le_one
added theorem finset.card_le_one_iff
added theorem finset.card_lt_card
added theorem finset.card_map
added theorem finset.card_mk
added theorem finset.card_mono
added theorem finset.card_pos
added theorem finset.card_range
added theorem finset.card_sdiff
added theorem finset.card_singleton
added theorem finset.card_subtype
added theorem finset.card_union_eq
added theorem finset.card_union_le
added theorem finset.filter_card_eq
added theorem finset.length_to_list
added theorem finset.lt_wf
added theorem finset.one_lt_card
added theorem finset.one_lt_card_iff
added theorem list.card_to_finset
added theorem list.to_finset_card_le
added theorem finset.card_attach_fin
added theorem finset.coe_fin_range
added def finset.fin_range
added theorem finset.fin_range_card
added theorem finset.mem_attach_fin
added theorem finset.mem_fin_range