Commit 2024-09-25 08:40 1fc8e52b
View on Github →feat (MeasureTheory): Integrability and integral when the domain is empty. (#15459)
- Add
Integrable.of_isEmpty
. - Add
integral_of_isEmpty
.
feat (MeasureTheory): Integrability and integral when the domain is empty. (#15459)
Integrable.of_isEmpty
.integral_of_isEmpty
.