Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 07:55 2f342b80

View on Github →

feat(measure_theory): generalize some lemmas to outer_measure (#11501)

Estimated changes

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.measure_union_eq_top_iff

modified theorem measure_theory.measure_union_lt_top_iff

modified theorem measure_theory.measure_union_null_iff

Modified src/measure_theory/measure/outer_measure.lean

modified theorem measure_theory.outer_measure.Union_null

added theorem measure_theory.outer_measure.Union_null_iff

added theorem measure_theory.outer_measure.bUnion_null_iff

added theorem measure_theory.outer_measure.mono_null

added theorem measure_theory.outer_measure.sUnion_null_iff

added theorem measure_theory.outer_measure.univ_eq_zero_iff