Commit 2026-04-11 09:33 482345f7

View on Github →

chore(Order/Interval/Finset/Defs): use to_dual (#37837) This PR uses to_dual on finite intervals. In particular, this fixes the leaky instance on LocallyFiniteOrder (WithBot α). Lemmas Iio_eq_Ico and Iic_eq_Icc were previously stated in not-fully-applied form. This is not compatible with their dual version, so this PR makes them be fully applied. I also changed Finset.range_eq_Ico and friends to be fully applied. I think this is better for consistency.

Estimated changes

deleted theorem Finset.Ici_toDual
deleted def Finset.Iic
deleted theorem Finset.Iic_eq_Icc
deleted theorem Finset.Iic_ofDual
deleted theorem Finset.Iic_prod_def
deleted theorem Finset.Iic_product_Iic
deleted def Finset.Iio
deleted theorem Finset.Iio_eq_Ico
deleted theorem Finset.Iio_ofDual
deleted theorem Finset.Ioc_ofDual
deleted theorem Finset.Ioc_orderDual_def
deleted theorem Finset.Ioc_toDual
deleted theorem Finset.Ioi_toDual
deleted theorem Finset.card_Iic_prod
deleted theorem Finset.coe_Iic
deleted theorem Finset.coe_Iio
deleted theorem Finset.coe_Ioc
added theorem Finset.mem_Icc'
added theorem Finset.mem_Ico'
deleted theorem Finset.mem_Iic
deleted theorem Finset.mem_Iio
added theorem Finset.mem_Ioc'
added theorem Finset.mem_Ioo'
deleted theorem Finset.subtype_Iic_eq
deleted theorem Finset.subtype_Iio_eq
deleted theorem Finset.subtype_Ioc_eq
deleted theorem Fintype.card_Iic
deleted theorem Fintype.card_Iio
deleted theorem Fintype.card_Ioc
deleted theorem Ici_orderDual_def
deleted theorem Ioi_orderDual_def
modified theorem Set.finite_Icc
modified theorem Set.finite_Ici
modified theorem Set.finite_Ico
deleted theorem Set.finite_Iic
deleted theorem Set.finite_Iio
deleted theorem Set.finite_Ioc
modified theorem Set.finite_Ioi
modified theorem Set.finite_Ioo
deleted theorem Set.finite_iff_bddBelow
modified theorem Set.toFinset_Icc
modified theorem Set.toFinset_Ico
deleted theorem Set.toFinset_Iic
deleted theorem Set.toFinset_Iio
deleted theorem Set.toFinset_Ioc
modified theorem Set.toFinset_Ioo
deleted theorem WithBot.Icc_bot_coe
deleted theorem WithBot.Icc_coe_coe
deleted theorem WithBot.Ico_bot_coe
deleted theorem WithBot.Ico_coe_coe
deleted theorem WithBot.Ioc_bot_coe
deleted theorem WithBot.Ioc_coe_coe
deleted theorem WithBot.Ioo_bot_coe
deleted theorem WithBot.Ioo_coe_coe
deleted theorem WithBot.bot_mem_insertBot
deleted def WithBot.insertBot
modified theorem Finset.range_eq_Ico
modified theorem Nat.Ico_zero_eq_range
modified theorem Nat.Iio_eq_range