Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-13 22:32 a359bd98

View on Github →

chore(measure_theory): measurability statements for coercions, coherent naming (#7854) Also add a few lemmas on measure theory

Estimated changes

Modified src/algebra/ordered_group.lean

added theorem max_zero_sub_max_neg_zero_eq_self

Modified src/analysis/mean_inequalities.lean

Modified src/analysis/special_functions/pow.lean

Modified src/data/real/nnreal.lean

Modified src/measure_theory/bochner_integration.lean

added theorem measure_theory.integral_eq_integral_pos_part_sub_integral_neg_part

Modified src/measure_theory/borel_space.lean

added theorem ae_measurable.coe_ereal_ennreal

added theorem ae_measurable.coe_nnreal_ennreal

added theorem ae_measurable.coe_nnreal_real

added theorem ae_measurable.coe_real_ereal

deleted theorem ae_measurable.ennreal_coe

added theorem ae_measurable.ennreal_to_nnreal

added theorem ae_measurable.ennreal_to_real

added theorem ae_measurable.ereal_to_real

deleted theorem ae_measurable.nnreal_coe

deleted theorem ae_measurable.to_real

deleted theorem ennreal.measurable_coe

added theorem ereal.measurable_of_measurable_real

added theorem lower_semicontinuous.measurable

added theorem measurable.coe_ereal_ennreal

added theorem measurable.coe_nnreal_ennreal

added theorem measurable.coe_nnreal_real

added theorem measurable.coe_real_ereal

deleted theorem measurable.ennreal_coe

added theorem measurable.ennreal_to_nnreal

added theorem measurable.ennreal_to_real

added theorem measurable.ereal_to_real

deleted theorem measurable.nnreal_coe

deleted theorem measurable.to_nnreal

deleted theorem measurable.to_real

added theorem measurable_coe_ennreal_ereal

added theorem measurable_coe_nnreal_ennreal

added theorem measurable_coe_nnreal_ennreal_iff

added theorem measurable_coe_nnreal_real

added theorem measurable_coe_real_ereal

deleted theorem measurable_ennreal_coe_iff

added def measurable_equiv.ereal_equiv_real

added theorem measurable_ereal_to_real

added theorem measurable_real_to_nnreal

deleted theorem nnreal.measurable_coe

added theorem upper_semicontinuous.measurable

Modified src/measure_theory/integration.lean

Modified src/measure_theory/l1_space.lean

added theorem measure_theory.integrable.real_to_nnreal

Modified src/measure_theory/measurable_space.lean

added theorem measurable_of_fintype

added theorem measurable_of_measurable_on_compl_finite

Modified src/measure_theory/prod.lean

Modified src/topology/metric_space/basic.lean

added theorem coe_nnreal_ennreal_nndist

deleted theorem ennreal_coe_nndist