Theorem IntervalIntegrable.def'

Modification history

2024-03-21 08:50
Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
chore: rename away from 'def' (#11548) …
Added IntervalIntegrable.def'View on Github →