Theorem WithBot.range_coe

Modification history

2025-10-16 16:35
Mathlib/Order/Interval/Set/WithBotTop.lean
refactor: define `≤`/`<` on `WithBot`/`WithTop` by induction (#19668) …
Modified WithBot.range_coeView on Github →
2022-12-17 23:34
Mathlib/Data/Set/Intervals/WithBotTop.lean
feat: port Data.Set.Intervals.WithBotTop (#1072)
Added WithBot.range_coeView on Github →