mathlib
8b8ba04e - feat (measure_theory/integral): lemmas `integral_Ioi_eq_integral_Ici` etc (#18899)

Commit
2 years ago
feat (measure_theory/integral): lemmas `integral_Ioi_eq_integral_Ici` etc (#18899) We already have some lemmas relating integrals over open vs. closed intervals, but some were missing (notably half-infinite integrals). This should now be a full set. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading