Commit 2020-10-17 23:24 13cd192e

View on Github →

feat(measure_theory/measure_space): added sub for measure_theory.measure (#4639) This definition is useful for proving the Lebesgue-Radon-Nikodym theorem for non-negative measures.

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.le_of_add_le_add_left

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure.le_of_add_le_add_left

added theorem measure_theory.measure.le_zero_iff_eq'

added theorem measure_theory.measure.sub_add_cancel_of_le

added theorem measure_theory.measure.sub_apply

added theorem measure_theory.measure.sub_def

added theorem measure_theory.measure.sub_eq_zero_of_le

Modified src/topology/instances/ennreal.lean

added theorem ennreal.tsum_sub