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 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 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
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