Theorem Set.Nonempty.ordConnected_iff_of_bdd'

Modification history

2025-04-15 10:53
Mathlib/Order/Interval/Set/OrdConnectedLinear.lean
feat: add characterisation of closed interval for locally-finite conditionally complete linear orders (#23910)
Added Set.Nonempty.ordConnected_iff_of_bdd'View on Github →