mathlib3
7a8a9146
- refactor(measure_theory/function/l1_space): remove hypothesis (#10185)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
refactor(measure_theory/function/l1_space): remove hypothesis (#10185) * from `tendsto_lintegral_norm_of_dominated_convergence` * Missed this in #10181 * Add comment about the ability to weaker `bound_integrable`.
Author
fpvandoorn
Parents
7d240ce1
Loading