Commit 2025-09-11 07:52 0b0e1dd6

View on Github →

feat: the topology on WithTop is second countable (#29466)

Estimated changes

added theorem WithBot.Icc_coe
added theorem WithBot.Ici_coe
added theorem WithBot.Ico_coe
added theorem WithBot.Iic_coe
added theorem WithBot.Iio_coe
added theorem WithBot.Ioc_coe
added theorem WithBot.Ioi_coe
added theorem WithBot.Ioo_coe
added theorem WithTop.Icc_coe
added theorem WithTop.Ici_coe
added theorem WithTop.Ico_coe
added theorem WithTop.Iic_coe
added theorem WithTop.Iio_coe
added theorem WithTop.Ioc_coe
added theorem WithTop.Ioi_coe
added theorem WithTop.Ioo_coe
added theorem isOpen_Iio'
added theorem isOpen_Ioi'