Commit 2026-04-21 17:27 4c9893d1

View on Github →

chore(Order/Interval/Set/WithBotTop): use to_dual (#38240)

Estimated changes

deleted theorem WithBot.bot_covBy_coe
deleted theorem WithBot.bot_wcovBy_coe
deleted theorem WithBot.coe_covBy_coe
deleted theorem WithBot.coe_wcovBy_coe
modified theorem WithTop.coe_covBy_coe
modified theorem WithTop.coe_covBy_top
modified theorem WithTop.coe_wcovBy_coe
modified theorem WithTop.coe_wcovBy_top
deleted theorem Set.ordConnected_Icc
deleted theorem Set.ordConnected_Ici
deleted theorem Set.ordConnected_Ico
deleted theorem Set.ordConnected_Iic
deleted theorem Set.ordConnected_Iio
deleted theorem Set.ordConnected_Ioc
deleted theorem Set.ordConnected_Ioi
deleted theorem Set.ordConnected_Ioo
deleted theorem WithBot.Icc_coe
deleted theorem WithBot.Ici_coe
deleted theorem WithBot.Ico_coe
deleted theorem WithBot.Iic_coe
deleted theorem WithBot.Iio_coe
deleted theorem WithBot.Ioc_coe
deleted theorem WithBot.Ioi_coe
deleted theorem WithBot.Ioo_coe
deleted theorem WithBot.image_coe_Icc
deleted theorem WithBot.image_coe_Ici
deleted theorem WithBot.image_coe_Ico
deleted theorem WithBot.image_coe_Iic
deleted theorem WithBot.image_coe_Iio
deleted theorem WithBot.image_coe_Ioc
deleted theorem WithBot.image_coe_Ioi
deleted theorem WithBot.image_coe_Ioo
deleted theorem WithBot.preimage_coe_Icc
deleted theorem WithBot.preimage_coe_Ici
deleted theorem WithBot.preimage_coe_Ico
deleted theorem WithBot.preimage_coe_Iic
deleted theorem WithBot.preimage_coe_Iio
deleted theorem WithBot.preimage_coe_Ioc
deleted theorem WithBot.preimage_coe_Ioi
deleted theorem WithBot.preimage_coe_Ioo
deleted theorem WithBot.preimage_coe_bot
deleted theorem WithBot.range_coe