Commit 2025-03-05 06:23 7fd25592

View on Github →

feat(Finset): Ioc a b is disjoint from Ioc c d when b ≤ c (#22552)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Partition/Basic.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/Order/Interval/Finset/Basic.lean

added theorem Finset.Ioc_disjoint_Ioc

added theorem Finset.Ioc_disjoint_Ioc_of_le

added theorem Finset.Ioc_inter_Ioc

Modified Mathlib/Order/Interval/Set/Disjoint.lean

added theorem Set.Ioc_disjoint_Ioc_of_le