Zulip Chat Archive
Stream: Is there code for X?
Topic: Set being an interval
Daniel Weber (Aug 31 2024 at 02:46):
We can say that a set is an interval if for any a ≤ b ≤ c, if the set contains a and c, then it contains b. Is this predicate in Mathlib?
Daniel Weber (Aug 31 2024 at 03:13):
nevermind, I found docs#Set.OrdConnected
Last updated: May 02 2025 at 03:31 UTC