Commit 2025-03-27 07:33 75a21e95

View on Github →

chore: rename Set.dual_Ixx to Ixx_toDual, and add Set.Ixx_ofDual (#23126) This is an excursion during the erw-killing quest.

Estimated changes

added theorem Set.Icc_ofDual
added theorem Set.Icc_toDual
added theorem Set.Ici_ofDual
added theorem Set.Ici_toDual
added theorem Set.Ico_ofDual
added theorem Set.Ico_toDual
added theorem Set.Iic_ofDual
added theorem Set.Iic_toDual
added theorem Set.Iio_ofDual
added theorem Set.Iio_toDual
added theorem Set.Ioc_ofDual
added theorem Set.Ioc_toDual
added theorem Set.Ioi_ofDual
added theorem Set.Ioi_toDual
added theorem Set.Ioo_ofDual
added theorem Set.Ioo_toDual
deleted theorem Set.dual_Icc
deleted theorem Set.dual_Ici
deleted theorem Set.dual_Ico
deleted theorem Set.dual_Iic
deleted theorem Set.dual_Iio
deleted theorem Set.dual_Ioc
deleted theorem Set.dual_Ioi
deleted theorem Set.dual_Ioo
deleted theorem Set.dual_uIcc
deleted theorem Set.dual_uIoo
added theorem Set.uIcc_ofDual
added theorem Set.uIcc_toDual
added theorem Set.uIoo_ofDual
added theorem Set.uIoo_toDual