Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-17 18:46 c8ae79d0

View on Github →

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

Estimated changes

Modified src/measure_theory/bochner_integration.lean

added theorem measure_theory.tendsto_integral_filter_of_dominated_convergence

modified theorem measure_theory.tendsto_integral_of_dominated_convergence

Modified src/measure_theory/integration.lean

added theorem measure_theory.tendsto_lintegral_filter_of_dominated_convergence

Modified src/measure_theory/l1_space.lean

Modified src/topology/bases.lean

added theorem filter.has_countable_basis.tendsto_iff_seq_tendsto

added theorem filter.has_countable_basis.tendsto_of_seq_tendsto