Commit 2026-03-20 05:22 74ba8017

View on Github →

feat(Order/Interval/Set/Linearorder): use to_dual (#36821) This PR is subset of #35635. As was observed in that PR, some declarations in this file are annoying to tag. So, this PR adds only those to_dual tags which are obviously beneficial. The rest can be done later if desired.

Estimated changes

deleted theorem Set.Iic_diff_Iic
deleted theorem Set.Iic_diff_Iio
deleted theorem Set.Iio_diff_Iic
deleted theorem Set.Iio_diff_Iio
deleted theorem Set.Iio_inj
deleted theorem Set.Iio_injective
deleted theorem Set.Iio_inter_Iio
deleted theorem Set.Iio_ssubset_Iio_iff
deleted theorem Set.Iio_subset_Iic_iff
deleted theorem Set.Iio_subset_Iio_iff
deleted theorem Set.Ioc_inter_Ioc
deleted theorem Set.Ioi_inter_Ioo
deleted theorem Set.Ioo_inter_Ioi