Commit 2025-04-14 15:20 6369e448

View on Github →

feat(IntervalIntegral): add IntervalIntegrable.trans_iff etc (#24009)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

added theorem IntervalIntegrable.comp_sub_left_iff

added theorem IntervalIntegrable.symm_iff

added theorem IntervalIntegrable.trans_iff

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

added theorem Set.uIoc_union_uIoc