mathlib

c8ae79d0 - feat(measure_theory/bochner_integration): dominated convergence theorem for filters (#1884)

feat(measure_theory/bochner_integration): dominated convergence theorem for filters (#1884) * Dominated convergence theorem for filters * Update bases.lean * Update bochner_integration.lean * reviewer's comments Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>