Theorem Finset.Ioc_disjoint_Ioc_of_le

Modification history

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