Commit 2026-02-10 16:30 75d3f74e

View on Github →

feat(Order/Interval/Set): to_dual for Iio/Iic (#33964) This PR tags Iio/Ioi and Iic/Ici with to_dual. A future PR will do this for Ioc/Ico and Ioo and Icc.

Estimated changes

deleted theorem IsBot.Ici_eq
deleted theorem IsMax.Ici_eq
deleted theorem Set.Ici_bot
deleted theorem Set.Ici_diff_Ioi_same
deleted theorem Set.Ici_diff_left
deleted theorem Set.Ici_inj
deleted theorem Set.Ici_injective
deleted theorem Set.Ici_inter_Ici
deleted theorem Set.Ici_ofDual
deleted theorem Set.Ici_prod_Ici
deleted theorem Set.Ici_prod_eq
deleted theorem Set.Ici_ssubset_Ici
deleted theorem Set.Ici_subset_Ici
deleted theorem Set.Ici_subset_Ioi
deleted theorem Set.Ici_toDual
deleted theorem Set.Iic_bot
modified theorem Set.Iic_ssubset_Iic
deleted theorem Set.Iio_bot
modified theorem Set.Iio_eq_empty_iff
modified theorem Set.Iio_nonempty
deleted theorem Set.Ioi_bot
deleted theorem Set.Ioi_eq_empty_iff
deleted theorem Set.Ioi_insert
deleted theorem Set.Ioi_nonempty
deleted theorem Set.Ioi_ofDual
deleted theorem Set.Ioi_ssubset_Ici_self
deleted theorem Set.Ioi_ssubset_Ioi
deleted theorem Set.Ioi_subset_Ici
deleted theorem Set.Ioi_subset_Ici_self
deleted theorem Set.Ioi_subset_Ioi
deleted theorem Set.Ioi_toDual
deleted theorem Set.Ioi_union_left
deleted theorem Set.nonempty_Ici
deleted theorem Set.nonempty_Ioi
deleted theorem Set.notMem_Iio_self
deleted theorem Set.notMem_Ioi_self
deleted theorem Set.self_mem_Ici
modified theorem Set.self_mem_Iic
modified theorem Set.self_notMem_Iio
deleted theorem Set.self_notMem_Ioi