Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-25 17:50 315a6427

View on Github →

feat(measure_theory): add Hahn decomposition

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.to_nnreal_add

Modified src/data/real/nnreal.lean

added theorem nnreal.coe_nonneg

Created src/measure_theory/decomposition.lean

added theorem measure_theory.hahn_decomposition

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.measure_eq_inter_diff

added theorem measure_theory.tendsto_measure_Inter

added theorem measure_theory.tendsto_measure_Union

added theorem tendsto_at_top_infi_nat

added theorem tendsto_at_top_supr_nat