Theorem Set.Ioc_disjoint_Ioc_of_le

Modification history

2025-03-05 06:23
Mathlib/Order/Interval/Set/Disjoint.lean
feat(Finset): `Ioc a b` is disjoint from `Ioc c d` when `b ≤ c` (#22552)
Added Set.Ioc_disjoint_Ioc_of_leView on Github →