Commit 2023-05-06 11:29 b1a047ac

View on Github →

feat: port MeasureTheory.Measure.NullMeasurable (#3349)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/NullMeasurable.lean

added theorem Finset.nullMeasurableSet_binterᵢ

added theorem Finset.nullMeasurableSet_bunionᵢ

added theorem Measurable.congr_ae

added theorem MeasurableSet.nullMeasurableSet

added theorem MeasureTheory.Measurable.comp_nullMeasurable

added theorem MeasureTheory.Measure.IsComplete.out

added theorem MeasureTheory.Measure.coe_completion

added def MeasureTheory.Measure.completion

added theorem MeasureTheory.Measure.completion_apply

added theorem MeasureTheory.Measure.isComplete_iff

added theorem MeasureTheory.NullMeasurable.congr

added theorem MeasureTheory.NullMeasurable.measurable_of_complete

added def MeasureTheory.NullMeasurable

added theorem MeasureTheory.NullMeasurableSet.compl

added theorem MeasureTheory.NullMeasurableSet.compl_iff

added theorem MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq

added theorem MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq

added theorem MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq

added theorem MeasureTheory.NullMeasurableSet.measurable_of_complete

added theorem MeasureTheory.NullMeasurableSet.of_compl

added theorem MeasureTheory.NullMeasurableSet.of_null

added theorem MeasureTheory.NullMeasurableSet.of_subsingleton

added theorem MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq

added def MeasureTheory.NullMeasurableSet

added def MeasureTheory.NullMeasurableSpace

added theorem MeasureTheory.exists_subordinate_pairwise_disjoint

added theorem MeasureTheory.measurableSet_of_null

added theorem MeasureTheory.measure_add_measure_compl₀

added theorem MeasureTheory.measure_inter_add_diff₀

added theorem MeasureTheory.measure_union_add_inter₀'

added theorem MeasureTheory.measure_union_add_inter₀

added theorem MeasureTheory.measure_unionᵢ

added theorem MeasureTheory.measure_unionᵢ₀

added theorem MeasureTheory.measure_union₀'

added theorem MeasureTheory.measure_union₀

added theorem MeasureTheory.measure_union₀_aux

added theorem MeasureTheory.nullMeasurableSet_empty

added theorem MeasureTheory.nullMeasurableSet_eq

added theorem MeasureTheory.nullMeasurableSet_insert

added theorem MeasureTheory.nullMeasurableSet_singleton

added theorem MeasureTheory.nullMeasurableSet_to_measurable

added theorem MeasureTheory.nullMeasurableSet_univ

added theorem Set.Finite.nullMeasurableSet_binterᵢ

added theorem Set.Finite.nullMeasurableSet_bunionᵢ

added theorem Set.Finite.nullMeasurableSet_interₛ

added theorem Set.Finite.nullMeasurableSet_unionₛ