Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-23 12:13 2b35fc7b

View on Github →

refactor(data/set/finite): reorganize and put emphasis on fintype instances (#14136) I went through data/set/finite and reorganized it by rough topic (and moved some lemmas to their proper homes; closes #11177). Two important parts of this module are (1) fintype instances for various set constructions and (2) ways to create set.finite terms. This change puts the module closer to following a design where the set.finite terms are created in a formulaic way from the fintype instances. One tool for this is a set.finite_of_fintype constructor, which lets typeclass inference do most of the work. Included in this commit is changing set.infinite to be protected so that it does not conflict with infinite.

Estimated changes

added theorem set.to_finset_diff
added theorem set.to_finset_insert
added theorem set.to_finset_inter
modified theorem set.to_finset_range
added theorem set.to_finset_union
modified theorem set.to_finset_univ
modified theorem finset.finite_to_set
deleted theorem set.card_fintype_insert'
added theorem set.finite.bUnion'
modified theorem set.finite.bUnion
modified theorem set.finite.bind
modified theorem set.finite.coe_to_finset
modified theorem set.finite.dependent_image
added theorem set.finite.diff
modified theorem set.finite.dinduction_on
modified theorem set.finite.exists_finset
modified theorem set.finite.fin_param
modified theorem set.finite.image2
modified theorem set.finite.image
modified theorem set.finite.induction_on
modified theorem set.finite.infinite_compl
modified theorem set.finite.insert
modified theorem set.finite.inter_of_left
modified theorem set.finite.inter_of_right
modified theorem set.finite.map
modified theorem set.finite.mem_to_finset
modified theorem set.finite.of_diff
modified theorem set.finite.of_fintype
modified theorem set.finite.of_preimage
modified theorem set.finite.prod
modified theorem set.finite.sInter
modified theorem set.finite.sUnion
added theorem set.finite.sep
modified theorem set.finite.seq'
modified theorem set.finite.seq
modified theorem set.finite.subset
modified theorem set.finite.to_finset_inj
modified theorem set.finite.to_finset_mono
modified theorem set.finite.union
modified theorem set.finite_Union
modified theorem set.finite_def
modified theorem set.finite_empty
modified theorem set.finite_empty_to_finset
modified theorem set.finite_le_nat
modified theorem set.finite_lt_nat
modified theorem set.finite_mem_finset
added theorem set.finite_of_fintype
modified theorem set.finite_option
modified theorem set.finite_pure
modified theorem set.finite_range
modified theorem set.finite_singleton
modified theorem set.finite_union
modified theorem set.finite_univ
modified def set.fintype_bUnion
deleted def set.fintype_insert'
modified theorem set.infinite.diff
modified theorem set.infinite.exists_nat_lt
modified theorem set.infinite.to_subtype
deleted def set.infinite
modified theorem set.infinite_coe_iff
modified theorem set.infinite_union
modified theorem set.infinite_univ
modified theorem set.infinite_univ_iff
deleted theorem set.insert_to_finset
modified theorem set.not_infinite
modified theorem set.subset_to_finset_iff
deleted theorem set.to_finset_insert
deleted theorem set.to_finset_inter
deleted theorem set.to_finset_ne_eq_erase
deleted theorem set.to_finset_sdiff
deleted theorem set.to_finset_singleton
deleted theorem set.to_finset_union
modified theorem set.Icc.infinite
modified theorem set.Ici.infinite
modified theorem set.Ico.infinite
modified theorem set.Iic.infinite
modified theorem set.Iio.infinite
modified theorem set.Ioc.infinite
modified theorem set.Ioi.infinite
modified theorem set.Ioo.infinite