Theorem WithBot.Ico_coe

Modification history

2026-04-21 17:27

Mathlib/Order/Interval/Set/WithBotTop.lean

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

Deleted WithBot.Ico_coe View on Github →

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 WithBot.Ico_coe View on Github →

2025-09-11 07:52

Mathlib/Order/Interval/Set/WithBotTop.lean

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

Added WithBot.Ico_coe View on Github →