Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-11 10:26 e4a882dd

View on Github →

feat(measure_theory): a file about null measurable sets/functions (#10231)

Move definitions and lemmas about null_measurable to a new file.
Redefine, rename, review API.

Estimated changes

Modified docs/overview.yaml

Modified src/algebra/support.lean

added theorem function.mul_support_eq_preimage

Modified src/measure_theory/integral/set_integral.lean

Modified src/measure_theory/measure/measure_space.lean

deleted def completion

deleted theorem measurable.ae_eq

deleted theorem measurable_set.diff_null

deleted theorem measurable_set.null_measurable_set

deleted theorem measure_theory.measure.is_complete.out

deleted theorem measure_theory.measure.is_complete_iff

added theorem measure_theory.measure.restrict_apply₀

deleted theorem measure_theory.measure_Union

added theorem measure_theory.null_measurable_set.mono

added theorem measure_theory.null_measurable_set.mono_ac

added theorem measure_theory.to_measure_apply₀

deleted def null_measurable

deleted theorem null_measurable_set.Union_nat

deleted theorem null_measurable_set.compl

deleted theorem null_measurable_set.diff_null

deleted theorem null_measurable_set.union_null

deleted def null_measurable_set

deleted theorem null_measurable_set_iff

deleted theorem null_measurable_set_iff_ae

deleted theorem null_measurable_set_iff_sandwich

deleted theorem null_measurable_set_measure_eq

deleted theorem null_measurable_set_of_complete

deleted theorem null_null_measurable_set

deleted theorem restrict_apply_of_null_measurable_set

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.ae_le_to_measurable

Created src/measure_theory/measure/null_measurable.lean

added theorem finset.null_measurable_set_bInter

added theorem finset.null_measurable_set_bUnion

added theorem measurable.congr_ae

added theorem measurable_set.null_measurable_set

added theorem measure_theory.measurable.comp_null_measurable

added theorem measure_theory.measurable_set_of_null

added theorem measure_theory.measure.coe_completion

added def measure_theory.measure.completion

added theorem measure_theory.measure.completion_apply

added theorem measure_theory.measure.is_complete.out

added theorem measure_theory.measure.is_complete_iff

added theorem measure_theory.measure_Union

added theorem measure_theory.measure_Union₀

added theorem measure_theory.measure_union₀

added theorem measure_theory.null_measurable.congr

added theorem measure_theory.null_measurable.measurable_of_complete

added def measure_theory.null_measurable

added theorem measure_theory.null_measurable_set.Inter_Prop

added theorem measure_theory.null_measurable_set.Inter_fintype

added theorem measure_theory.null_measurable_set.Union_Prop

added theorem measure_theory.null_measurable_set.Union_fintype

added theorem measure_theory.null_measurable_set.compl

added theorem measure_theory.null_measurable_set.compl_iff

added theorem measure_theory.null_measurable_set.compl_to_measurable_compl_ae_eq

added theorem measure_theory.null_measurable_set.exists_measurable_subset_ae_eq

added theorem measure_theory.null_measurable_set.exists_measurable_superset_ae_eq

added theorem measure_theory.null_measurable_set.measurable_of_complete

added theorem measure_theory.null_measurable_set.of_compl

added theorem measure_theory.null_measurable_set.of_null

added theorem measure_theory.null_measurable_set.of_subsingleton

added theorem measure_theory.null_measurable_set.to_measurable_ae_eq

added def measure_theory.null_measurable_set

added theorem measure_theory.null_measurable_set_empty

added theorem measure_theory.null_measurable_set_eq

added theorem measure_theory.null_measurable_set_insert

added theorem measure_theory.null_measurable_set_singleton

added theorem measure_theory.null_measurable_set_to_measurable

added theorem measure_theory.null_measurable_set_univ

added def measure_theory.null_measurable_space

added theorem set.finite.null_measurable_set_bInter

added theorem set.finite.null_measurable_set_bUnion

added theorem set.finite.null_measurable_set_sInter

added theorem set.finite.null_measurable_set_sUnion