Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 20:43 99881936

View on Github →

feat(measure_theory): various additions (#5389) Some computations of measures on non-measurable sets Some more measurability lemmas for pi-types Cleanup in measure_space

Estimated changes

modified def completion
modified theorem is_measurable.diff_null
modified theorem is_null_measurable.compl
modified def is_null_measurable
modified theorem is_null_measurable_iff
modified theorem measure_theory.ae_all_iff
modified theorem measure_theory.ae_ball_iff
modified theorem measure_theory.ae_eq_empty
modified theorem measure_theory.ae_eq_refl
modified theorem measure_theory.ae_eq_symm
modified theorem measure_theory.ae_eq_trans
modified theorem measure_theory.ae_le_set
modified theorem measure_theory.ae_map_iff
modified theorem measure_theory.ae_of_all
modified theorem measure_theory.measure.ext
modified theorem measure_theory.measure_diff
modified theorem measure_theory.measure_if
modified theorem null_is_null_measurable
modified def null_measurable