Commit 2025-10-10 07:59 702baa55

View on Github →

chore(Order/Interval/Set): golf entire {Icc,Ici,Ico,Iic,Iio,Ioc,Ioi,Ioo}_coe (#30268)

Estimated changes

modified theorem WithBot.Icc_coe
modified theorem WithBot.Ici_coe
modified theorem WithBot.Ico_coe
modified theorem WithBot.Ioc_coe
modified theorem WithBot.Ioi_coe
modified theorem WithBot.Ioo_coe
modified theorem WithTop.Icc_coe
modified theorem WithTop.Ico_coe
modified theorem WithTop.Iic_coe
modified theorem WithTop.Iio_coe
modified theorem WithTop.Ioc_coe
modified theorem WithTop.Ioo_coe