Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-03-12 20:45 5f8c26ce

View on Github →

feat(analysis/measure_theory): measures are embedded in outer measures; add map, dirac, and sum measures

Estimated changes

Modified analysis/ennreal.lean

added theorem ennreal.tsum_supr_eq

Modified analysis/measure_theory/measure_space.lean

deleted def measure_theory.count

added theorem measure_theory.le_to_outer_measure_caratheodory

added def measure_theory.measure_space.count

added def measure_theory.measure_space.dirac

added def measure_theory.measure_space.map

added theorem measure_theory.measure_space.map_comp

added theorem measure_theory.measure_space.map_id

added theorem measure_theory.measure_space.map_measure

added def measure_theory.measure_space.sum

added theorem measure_theory.to_outer_measure_to_measure