Theorem Set.ordConnected_Ico

Modification history

2026-04-21 17:27
Mathlib/Order/Interval/Set/OrdConnected.lean
chore(Order/Interval/Set/WithBotTop): use `to_dual` (#38240)
Deleted Set.ordConnected_IcoView on Github →
2022-12-30 11:50
Mathlib/Data/Set/Intervals/OrdConnected.lean
chore: various naming fixes (#1258)
Added Set.ordConnected_IcoView on Github →