Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-14 19:58 1d29de43

View on Github →

feat(data/*/interval): finset.uIcc on concrete structures (#18838) Calculate the size of finset.uIcc in ℕ, ℤ, fin, prod, pi, multiset, finset...

Estimated changes

added theorem dfinsupp.card_uIcc
added theorem fin.card_fintype_uIcc
added theorem fin.card_uIcc
added theorem fin.coe_inf
added theorem fin.coe_max
added theorem fin.coe_min
added theorem fin.coe_sup
modified theorem finset.mem_uIcc_of_ge
modified theorem finset.mem_uIcc_of_le
added theorem finsupp.card_uIcc
modified theorem int.card_Icc
modified theorem int.card_Ico
modified theorem int.card_Ioc
modified theorem int.card_Ioo
added theorem int.card_fintype_uIcc
added theorem int.card_uIcc
added theorem int.uIcc_eq_finset_map
added theorem multiset.card_uIcc
added theorem multiset.uIcc_eq
added theorem nat.card_uIcc
added theorem nat.uIcc_eq_range'
modified theorem pi.card_Ici
modified theorem pi.card_Ico
modified theorem pi.card_Iio
modified theorem pi.card_Ioc
modified theorem pi.card_Ioi
modified theorem pi.card_Ioo
added theorem pi.card_uIcc
added theorem pi.uIcc_eq
added theorem pnat.card_fintype_uIcc
added theorem pnat.card_uIcc
added theorem set.finite_interval