Theorem WithTop.Ico_coe

Modification history

2025-10-10 07:59
Mathlib/Order/Interval/Set/WithBotTop.lean
chore(Order/Interval/Set): golf entire `{Icc,Ici,Ico,Iic,Iio,Ioc,Ioi,Ioo}_coe` (#30268)
Modified WithTop.Ico_coeView on Github →
2025-09-11 07:52
Mathlib/Order/Interval/Set/WithBotTop.lean
feat: the topology on WithTop is second countable (#29466)
Added WithTop.Ico_coeView on Github →