Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 06:37 a98a26b2

View on Github →

chore(measure_theory): move lemmas about ae_measurable to a new file (#13246)

Estimated changes

Modified src/dynamics/ergodic/measure_preserving.lean

Modified src/measure_theory/group/arithmetic.lean

Modified src/measure_theory/lattice.lean

Created src/measure_theory/measure/ae_measurable.lean

added theorem ae_measurable.add_measure

added theorem ae_measurable.ae_inf_principal_eq_mk

added theorem ae_measurable.ae_mem_imp_eq_mk

added theorem ae_measurable.comp_measurable'

added theorem ae_measurable.comp_measurable

added theorem ae_measurable.exists_ae_eq_range_subset

added theorem ae_measurable.indicator

added theorem ae_measurable.mono_measure

added theorem ae_measurable.mono_set

added theorem ae_measurable.prod_mk

added theorem ae_measurable.restrict

added theorem ae_measurable.smul_measure

added theorem ae_measurable.subtype_mk

added theorem ae_measurable.sum_measure

added theorem ae_measurable_Union_iff

added theorem ae_measurable_add_measure_iff

added theorem ae_measurable_iff_measurable

added theorem ae_measurable_indicator_iff

added theorem ae_measurable_interval_oc_iff

added theorem ae_measurable_map_equiv_iff

added theorem ae_measurable_of_ae_measurable_trim

added theorem ae_measurable_of_subsingleton_codomain

added theorem ae_measurable_one

added theorem ae_measurable_restrict_iff_comap_subtype

added theorem ae_measurable_restrict_of_measurable_subtype

added theorem ae_measurable_smul_measure_iff

added theorem ae_measurable_sum_measure_iff

added theorem ae_measurable_union_iff

added theorem ae_measurable_zero_measure

added theorem measurable_embedding.ae_measurable_comp_iff

added theorem measurable_embedding.ae_measurable_map_iff

added theorem subsingleton.ae_measurable

Modified src/measure_theory/measure/measure_space.lean

deleted theorem ae_measurable.add_measure

deleted theorem ae_measurable.ae_inf_principal_eq_mk

deleted theorem ae_measurable.ae_mem_imp_eq_mk

deleted theorem ae_measurable.comp_measurable'

deleted theorem ae_measurable.comp_measurable

deleted theorem ae_measurable.exists_ae_eq_range_subset

deleted theorem ae_measurable.indicator

deleted theorem ae_measurable.mono_measure

deleted theorem ae_measurable.mono_set

deleted theorem ae_measurable.prod_mk

deleted theorem ae_measurable.restrict

deleted theorem ae_measurable.smul_measure

deleted theorem ae_measurable.subtype_mk

deleted theorem ae_measurable.sum_measure

deleted theorem ae_measurable_Union_iff

deleted theorem ae_measurable_add_measure_iff

deleted theorem ae_measurable_iff_measurable

deleted theorem ae_measurable_indicator_iff

deleted theorem ae_measurable_interval_oc_iff

deleted theorem ae_measurable_map_equiv_iff

deleted theorem ae_measurable_of_ae_measurable_trim

deleted theorem ae_measurable_of_subsingleton_codomain

deleted theorem ae_measurable_one

deleted theorem ae_measurable_restrict_iff_comap_subtype

deleted theorem ae_measurable_restrict_of_measurable_subtype

deleted theorem ae_measurable_smul_measure_iff

deleted theorem ae_measurable_sum_measure_iff

deleted theorem ae_measurable_union_iff

deleted theorem ae_measurable_zero_measure

deleted theorem measurable_embedding.ae_measurable_comp_iff

deleted theorem measurable_embedding.ae_measurable_map_iff

deleted theorem subsingleton.ae_measurable