Commit 2024-08-26 16:09 ea40e709

View on Github →

chore(Order/Interval/Finset/Defs): Clean up namespaces (#15831) Some lemmas were accidentally dropped in the Prod or root namespace

Estimated changes

added theorem Finset.Icc_ofDual
added theorem Finset.Icc_prod_def
added theorem Finset.Icc_product_Icc
added theorem Finset.Icc_toDual
added theorem Finset.Ici_ofDual
added theorem Finset.Ici_prod_def
added theorem Finset.Ici_product_Ici
added theorem Finset.Ici_toDual
added theorem Finset.Ico_ofDual
added theorem Finset.Ico_toDual
added theorem Finset.Iic_ofDual
added theorem Finset.Iic_prod_def
added theorem Finset.Iic_product_Iic
added theorem Finset.Iic_toDual
added theorem Finset.Iio_ofDual
added theorem Finset.Iio_toDual
added theorem Finset.Ioc_ofDual
added theorem Finset.Ioc_toDual
added theorem Finset.Ioi_ofDual
added theorem Finset.Ioi_toDual
added theorem Finset.Ioo_ofDual
added theorem Finset.Ioo_toDual
added theorem Finset.card_Icc_prod
added theorem Finset.card_Ici_prod
added theorem Finset.card_Iic_prod
added theorem Finset.card_uIcc_prod
added theorem Finset.uIcc_prod_def
deleted theorem Icc_ofDual
deleted theorem Icc_toDual
deleted theorem Ici_ofDual
deleted theorem Ici_toDual
deleted theorem Ico_ofDual
deleted theorem Ico_toDual
deleted theorem Iic_ofDual
deleted theorem Iic_toDual
deleted theorem Iio_ofDual
deleted theorem Iio_toDual
deleted theorem Ioc_ofDual
deleted theorem Ioc_toDual
deleted theorem Ioi_ofDual
deleted theorem Ioi_toDual
deleted theorem Ioo_ofDual
deleted theorem Ioo_toDual
deleted theorem Prod.Icc_eq
deleted theorem Prod.Icc_mk_mk
deleted theorem Prod.card_Icc
deleted theorem Prod.card_uIcc
deleted theorem Prod.uIcc_eq
deleted theorem Prod.uIcc_mk_mk