Commit 2023-05-04 08:44 8e9ff289

View on Github →

feat: port MeasureTheory.Measure.MeasureSpaceDef (#3325)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem AEMeasurable.ae_eq_mk

added theorem AEMeasurable.congr

added theorem AEMeasurable.measurable_mk

added def AEMeasurable.mk

added def AEMeasurable

added theorem Measurable.aemeasurable

added theorem Measurable.comp_aemeasurable

added def MeasureTheory.Measure.ae

added theorem MeasureTheory.Measure.ext

added theorem MeasureTheory.Measure.ext_iff

added def MeasureTheory.Measure.ofMeasurable

added theorem MeasureTheory.Measure.ofMeasurable_apply

added theorem MeasureTheory.Measure.toOuterMeasure_injective

added structure MeasureTheory.Measure

added theorem MeasureTheory.Set.mulIndicator_ae_eq_one

added theorem MeasureTheory.ae_all_iff

added theorem MeasureTheory.ae_ball_iff

added theorem MeasureTheory.ae_eq_empty

added theorem MeasureTheory.ae_eq_refl

added theorem MeasureTheory.ae_eq_set

added theorem MeasureTheory.ae_eq_set_compl

added theorem MeasureTheory.ae_eq_set_compl_compl

added theorem MeasureTheory.ae_eq_set_inter

added theorem MeasureTheory.ae_eq_set_union

added theorem MeasureTheory.ae_eq_symm

added theorem MeasureTheory.ae_eq_trans

added theorem MeasureTheory.ae_eq_univ

added theorem MeasureTheory.ae_iff

added theorem MeasureTheory.ae_le_of_ae_lt

added theorem MeasureTheory.ae_le_set

added theorem MeasureTheory.ae_le_set_inter

added theorem MeasureTheory.ae_le_set_union

added theorem MeasureTheory.ae_le_toMeasurable

added theorem MeasureTheory.ae_of_all

added theorem MeasureTheory.compl_mem_ae_iff

added theorem MeasureTheory.diff_ae_eq_self

added theorem MeasureTheory.diff_null_ae_eq_self

added theorem MeasureTheory.exists_measurable_superset

added theorem MeasureTheory.exists_measurable_superset_forall_eq

added theorem MeasureTheory.exists_measurable_superset_iff_measure_eq_zero

added theorem MeasureTheory.exists_measurable_superset_of_null

added theorem MeasureTheory.exists_measurable_superset₂

added theorem MeasureTheory.exists_measure_pos_of_not_measure_unionᵢ_null

added theorem MeasureTheory.frequently_ae_iff

added theorem MeasureTheory.frequently_ae_mem_iff

added theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_left

added theorem MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_right

added theorem MeasureTheory.inter_ae_eq_left_of_ae_eq_univ

added theorem MeasureTheory.inter_ae_eq_right_of_ae_eq_univ

added theorem MeasureTheory.measurableSet_toMeasurable

added theorem MeasureTheory.measure_bunionᵢ_finset_le

added theorem MeasureTheory.measure_bunionᵢ_le

added theorem MeasureTheory.measure_bunionᵢ_lt_top

added theorem MeasureTheory.measure_bunionᵢ_null_iff

added theorem MeasureTheory.measure_congr

added theorem MeasureTheory.measure_empty

added theorem MeasureTheory.measure_eq_extend

added theorem MeasureTheory.measure_eq_inducedOuterMeasure

added theorem MeasureTheory.measure_eq_infᵢ'

added theorem MeasureTheory.measure_eq_infᵢ

added theorem MeasureTheory.measure_eq_trim

added theorem MeasureTheory.measure_inter_lt_top_of_left_ne_top

added theorem MeasureTheory.measure_inter_lt_top_of_right_ne_top

added theorem MeasureTheory.measure_inter_null_of_null_left

added theorem MeasureTheory.measure_inter_null_of_null_right

added theorem MeasureTheory.measure_mono

added theorem MeasureTheory.measure_mono_ae

added theorem MeasureTheory.measure_mono_null

added theorem MeasureTheory.measure_mono_null_ae

added theorem MeasureTheory.measure_mono_top

added theorem MeasureTheory.measure_symmDiff_eq_zero_iff

added theorem MeasureTheory.measure_toMeasurable

added theorem MeasureTheory.measure_union_eq_top_iff

added theorem MeasureTheory.measure_union_le

added theorem MeasureTheory.measure_union_lt_top

added theorem MeasureTheory.measure_union_lt_top_iff

added theorem MeasureTheory.measure_union_ne_top

added theorem MeasureTheory.measure_union_null

added theorem MeasureTheory.measure_union_null_iff

added theorem MeasureTheory.measure_unionᵢ_fintype_le

added theorem MeasureTheory.measure_unionᵢ_le

added theorem MeasureTheory.measure_unionᵢ_null

added theorem MeasureTheory.measure_unionᵢ_null_iff'

added theorem MeasureTheory.measure_unionᵢ_null_iff

added theorem MeasureTheory.measure_unionₛ_null_iff

added theorem MeasureTheory.measure_zero_iff_ae_nmem

added theorem MeasureTheory.mem_ae_iff

added theorem MeasureTheory.nonempty_of_measure_ne_zero

added theorem MeasureTheory.subset_toMeasurable

added theorem MeasureTheory.toOuterMeasure_eq_inducedOuterMeasure

added theorem MeasureTheory.union_ae_eq_left_of_ae_eq_empty

added theorem MeasureTheory.union_ae_eq_right

added theorem MeasureTheory.union_ae_eq_right_of_ae_eq_empty

added theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_left

added theorem MeasureTheory.union_ae_eq_univ_of_ae_eq_univ_right

added theorem aemeasurable_congr

added theorem aemeasurable_const

added theorem aemeasurable_id'

added theorem aemeasurable_id