Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-30 09:54 4ea253b7

View on Github →

feat(measure_theory/integration): in a sigma finite space, there exists an integrable positive function (#7721)

Estimated changes

Modified src/measure_theory/borel_space.lean

added theorem measurable.nnreal_tsum

Modified src/measure_theory/integration.lean

added theorem measure_theory.exists_integrable_pos_of_sigma_finite

Modified src/topology/algebra/infinite_sum.lean

added theorem tsum_pos

Modified src/topology/instances/ennreal.lean

added theorem nnreal.has_sum_lt

added theorem nnreal.has_sum_strict_mono

added theorem nnreal.tsum_eq_to_nnreal_tsum

added theorem nnreal.tsum_lt_tsum

added theorem nnreal.tsum_pos

added theorem nnreal.tsum_strict_mono