Commit 2024-05-16 08:10 727c4bcd

View on Github →

refactor(MeasureTheory/OuterMeasure): split large file (#12939) This PR (which supersedes #12895) splits up OuterMeasure/Basic (1700 lines) into 5 pieces of < 500 lines each.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

deleted def MeasureTheory.OuterMeasure.IsCaratheodory

deleted theorem MeasureTheory.OuterMeasure.add_apply

deleted theorem MeasureTheory.OuterMeasure.biInf_apply'

deleted theorem MeasureTheory.OuterMeasure.biInf_apply

deleted def MeasureTheory.OuterMeasure.boundedBy

deleted theorem MeasureTheory.OuterMeasure.boundedBy_apply

deleted theorem MeasureTheory.OuterMeasure.boundedBy_caratheodory

deleted theorem MeasureTheory.OuterMeasure.boundedBy_eq

deleted theorem MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction

deleted theorem MeasureTheory.OuterMeasure.boundedBy_eq_self

deleted theorem MeasureTheory.OuterMeasure.boundedBy_le

deleted theorem MeasureTheory.OuterMeasure.boundedBy_top

deleted theorem MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter

deleted theorem MeasureTheory.OuterMeasure.boundedBy_zero

deleted def MeasureTheory.OuterMeasure.caratheodoryDynkin

deleted def MeasureTheory.OuterMeasure.coeFnAddMonoidHom

deleted theorem MeasureTheory.OuterMeasure.coe_add

deleted theorem MeasureTheory.OuterMeasure.coe_bot

deleted theorem MeasureTheory.OuterMeasure.coe_iSup

deleted theorem MeasureTheory.OuterMeasure.coe_smul

deleted theorem MeasureTheory.OuterMeasure.coe_zero

deleted def MeasureTheory.OuterMeasure.comap

deleted theorem MeasureTheory.OuterMeasure.comap_apply

deleted theorem MeasureTheory.OuterMeasure.comap_boundedBy

deleted theorem MeasureTheory.OuterMeasure.comap_iInf

deleted theorem MeasureTheory.OuterMeasure.comap_iSup

deleted theorem MeasureTheory.OuterMeasure.comap_map

deleted theorem MeasureTheory.OuterMeasure.comap_mono

deleted theorem MeasureTheory.OuterMeasure.comap_ofFunction

deleted theorem MeasureTheory.OuterMeasure.comap_top

deleted def MeasureTheory.OuterMeasure.dirac

deleted theorem MeasureTheory.OuterMeasure.dirac_apply

deleted theorem MeasureTheory.OuterMeasure.dirac_caratheodory

deleted theorem MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim

deleted theorem MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim

deleted theorem MeasureTheory.OuterMeasure.exists_measurable_superset_of_trim_eq_zero

deleted theorem MeasureTheory.OuterMeasure.f_iUnion

deleted theorem MeasureTheory.OuterMeasure.iInf_apply'

deleted theorem MeasureTheory.OuterMeasure.iInf_apply

deleted theorem MeasureTheory.OuterMeasure.iSup_apply

deleted theorem MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_compl

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_empty

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_nat

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_iff

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le'

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_inter

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_sum

deleted theorem MeasureTheory.OuterMeasure.isCaratheodory_union

deleted theorem MeasureTheory.OuterMeasure.isGreatest_ofFunction

deleted theorem MeasureTheory.OuterMeasure.le_add_caratheodory

deleted theorem MeasureTheory.OuterMeasure.le_boundedBy'

deleted theorem MeasureTheory.OuterMeasure.le_boundedBy

deleted theorem MeasureTheory.OuterMeasure.le_comap_map

deleted theorem MeasureTheory.OuterMeasure.le_ofFunction

deleted theorem MeasureTheory.OuterMeasure.le_smul_caratheodory

deleted theorem MeasureTheory.OuterMeasure.le_sum_caratheodory

deleted theorem MeasureTheory.OuterMeasure.le_trim

deleted theorem MeasureTheory.OuterMeasure.le_trim_iff

deleted def MeasureTheory.OuterMeasure.map

deleted theorem MeasureTheory.OuterMeasure.map_apply

deleted theorem MeasureTheory.OuterMeasure.map_biInf_comap

deleted theorem MeasureTheory.OuterMeasure.map_comap

deleted theorem MeasureTheory.OuterMeasure.map_comap_le

deleted theorem MeasureTheory.OuterMeasure.map_comap_of_surjective

deleted theorem MeasureTheory.OuterMeasure.map_iInf

deleted theorem MeasureTheory.OuterMeasure.map_iInf_comap

deleted theorem MeasureTheory.OuterMeasure.map_iInf_le

deleted theorem MeasureTheory.OuterMeasure.map_iSup

deleted theorem MeasureTheory.OuterMeasure.map_id

deleted theorem MeasureTheory.OuterMeasure.map_le_restrict_range

deleted theorem MeasureTheory.OuterMeasure.map_map

deleted theorem MeasureTheory.OuterMeasure.map_mono

deleted theorem MeasureTheory.OuterMeasure.map_ofFunction

deleted theorem MeasureTheory.OuterMeasure.map_ofFunction_le

deleted theorem MeasureTheory.OuterMeasure.map_sup

deleted theorem MeasureTheory.OuterMeasure.map_top

deleted theorem MeasureTheory.OuterMeasure.map_top_of_surjective

deleted theorem MeasureTheory.OuterMeasure.measure_inter_union

deleted theorem MeasureTheory.OuterMeasure.mono''

deleted theorem MeasureTheory.OuterMeasure.ofFunction_apply

deleted theorem MeasureTheory.OuterMeasure.ofFunction_caratheodory

deleted theorem MeasureTheory.OuterMeasure.ofFunction_eq

deleted theorem MeasureTheory.OuterMeasure.ofFunction_eq_sSup

deleted theorem MeasureTheory.OuterMeasure.ofFunction_le

deleted theorem MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter

deleted def MeasureTheory.OuterMeasure.restrict

deleted theorem MeasureTheory.OuterMeasure.restrict_apply

deleted theorem MeasureTheory.OuterMeasure.restrict_biInf

deleted theorem MeasureTheory.OuterMeasure.restrict_empty

deleted theorem MeasureTheory.OuterMeasure.restrict_iInf

deleted theorem MeasureTheory.OuterMeasure.restrict_iInf_restrict

deleted theorem MeasureTheory.OuterMeasure.restrict_iSup

deleted theorem MeasureTheory.OuterMeasure.restrict_le_self

deleted theorem MeasureTheory.OuterMeasure.restrict_mono

deleted theorem MeasureTheory.OuterMeasure.restrict_ofFunction

deleted theorem MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict

deleted theorem MeasureTheory.OuterMeasure.restrict_trim

deleted theorem MeasureTheory.OuterMeasure.restrict_univ

deleted def MeasureTheory.OuterMeasure.sInfGen

deleted theorem MeasureTheory.OuterMeasure.sInfGen_def

deleted theorem MeasureTheory.OuterMeasure.sInf_apply'

deleted theorem MeasureTheory.OuterMeasure.sInf_apply

deleted theorem MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen

deleted theorem MeasureTheory.OuterMeasure.sSup_apply

deleted theorem MeasureTheory.OuterMeasure.smul_apply

deleted theorem MeasureTheory.OuterMeasure.smul_boundedBy

deleted theorem MeasureTheory.OuterMeasure.smul_dirac_apply

deleted theorem MeasureTheory.OuterMeasure.smul_iSup

deleted theorem MeasureTheory.OuterMeasure.smul_ofFunction

deleted def MeasureTheory.OuterMeasure.sum

deleted theorem MeasureTheory.OuterMeasure.sum_apply

deleted theorem MeasureTheory.OuterMeasure.sup_apply

deleted theorem MeasureTheory.OuterMeasure.top_apply'

deleted theorem MeasureTheory.OuterMeasure.top_apply

deleted theorem MeasureTheory.OuterMeasure.top_caratheodory

deleted def MeasureTheory.OuterMeasure.trim

deleted theorem MeasureTheory.OuterMeasure.trim_add

deleted theorem MeasureTheory.OuterMeasure.trim_anti_measurableSpace

deleted theorem MeasureTheory.OuterMeasure.trim_binop

deleted theorem MeasureTheory.OuterMeasure.trim_congr

deleted theorem MeasureTheory.OuterMeasure.trim_eq

deleted theorem MeasureTheory.OuterMeasure.trim_eq_iInf'

deleted theorem MeasureTheory.OuterMeasure.trim_eq_iInf

deleted theorem MeasureTheory.OuterMeasure.trim_eq_trim_iff

deleted theorem MeasureTheory.OuterMeasure.trim_iSup

deleted theorem MeasureTheory.OuterMeasure.trim_le_trim_iff

deleted theorem MeasureTheory.OuterMeasure.trim_mono

deleted theorem MeasureTheory.OuterMeasure.trim_op

deleted theorem MeasureTheory.OuterMeasure.trim_smul

deleted theorem MeasureTheory.OuterMeasure.trim_sum_ge

deleted theorem MeasureTheory.OuterMeasure.trim_sup

deleted theorem MeasureTheory.OuterMeasure.trim_top

deleted theorem MeasureTheory.OuterMeasure.trim_trim

deleted theorem MeasureTheory.OuterMeasure.trim_zero

deleted theorem MeasureTheory.OuterMeasure.univ_eq_zero_iff

deleted theorem MeasureTheory.OuterMeasure.zero_caratheodory

deleted def MeasureTheory.extend

deleted theorem MeasureTheory.extend_congr

deleted theorem MeasureTheory.extend_empty

deleted theorem MeasureTheory.extend_eq

deleted theorem MeasureTheory.extend_eq_top

deleted theorem MeasureTheory.extend_iUnion

deleted theorem MeasureTheory.extend_iUnion_le_tsum_nat'

deleted theorem MeasureTheory.extend_iUnion_le_tsum_nat

deleted theorem MeasureTheory.extend_iUnion_nat

deleted theorem MeasureTheory.extend_mono'

deleted theorem MeasureTheory.extend_mono

deleted theorem MeasureTheory.extend_top

deleted theorem MeasureTheory.extend_union

deleted def MeasureTheory.inducedOuterMeasure

deleted theorem MeasureTheory.inducedOuterMeasure_caratheodory

deleted theorem MeasureTheory.inducedOuterMeasure_eq'

deleted theorem MeasureTheory.inducedOuterMeasure_eq

deleted theorem MeasureTheory.inducedOuterMeasure_eq_extend'

deleted theorem MeasureTheory.inducedOuterMeasure_eq_extend

deleted theorem MeasureTheory.inducedOuterMeasure_eq_iInf

deleted theorem MeasureTheory.inducedOuterMeasure_exists_set

deleted theorem MeasureTheory.inducedOuterMeasure_preimage

deleted theorem MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter

deleted theorem MeasureTheory.le_extend

deleted theorem MeasureTheory.le_inducedOuterMeasure

deleted theorem MeasureTheory.smul_extend

Created Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

added def MeasureTheory.OuterMeasure.IsCaratheodory

added theorem MeasureTheory.OuterMeasure.boundedBy_caratheodory

added def MeasureTheory.OuterMeasure.caratheodoryDynkin

added theorem MeasureTheory.OuterMeasure.dirac_caratheodory

added theorem MeasureTheory.OuterMeasure.f_iUnion

added theorem MeasureTheory.OuterMeasure.isCaratheodory_compl

added theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff

added theorem MeasureTheory.OuterMeasure.isCaratheodory_empty

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_nat

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iff

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le'

added theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le

added theorem MeasureTheory.OuterMeasure.isCaratheodory_inter

added theorem MeasureTheory.OuterMeasure.isCaratheodory_sum

added theorem MeasureTheory.OuterMeasure.isCaratheodory_union

added theorem MeasureTheory.OuterMeasure.le_add_caratheodory

added theorem MeasureTheory.OuterMeasure.le_smul_caratheodory

added theorem MeasureTheory.OuterMeasure.le_sum_caratheodory

added theorem MeasureTheory.OuterMeasure.measure_inter_union

added theorem MeasureTheory.OuterMeasure.ofFunction_caratheodory

added theorem MeasureTheory.OuterMeasure.top_caratheodory

added theorem MeasureTheory.OuterMeasure.zero_caratheodory

Created Mathlib/MeasureTheory/OuterMeasure/Induced.lean

added theorem MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim

added theorem MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim

added theorem MeasureTheory.OuterMeasure.exists_measurable_superset_of_trim_eq_zero

added theorem MeasureTheory.OuterMeasure.le_trim

added theorem MeasureTheory.OuterMeasure.le_trim_iff

added theorem MeasureTheory.OuterMeasure.restrict_trim

added def MeasureTheory.OuterMeasure.trim

added theorem MeasureTheory.OuterMeasure.trim_add

added theorem MeasureTheory.OuterMeasure.trim_anti_measurableSpace

added theorem MeasureTheory.OuterMeasure.trim_binop

added theorem MeasureTheory.OuterMeasure.trim_congr

added theorem MeasureTheory.OuterMeasure.trim_eq

added theorem MeasureTheory.OuterMeasure.trim_eq_iInf'

added theorem MeasureTheory.OuterMeasure.trim_eq_iInf

added theorem MeasureTheory.OuterMeasure.trim_eq_trim_iff

added theorem MeasureTheory.OuterMeasure.trim_iSup

added theorem MeasureTheory.OuterMeasure.trim_le_trim_iff

added theorem MeasureTheory.OuterMeasure.trim_mono

added theorem MeasureTheory.OuterMeasure.trim_op

added theorem MeasureTheory.OuterMeasure.trim_smul

added theorem MeasureTheory.OuterMeasure.trim_sum_ge

added theorem MeasureTheory.OuterMeasure.trim_sup

added theorem MeasureTheory.OuterMeasure.trim_top

added theorem MeasureTheory.OuterMeasure.trim_trim

added theorem MeasureTheory.OuterMeasure.trim_zero

added def MeasureTheory.extend

added theorem MeasureTheory.extend_congr

added theorem MeasureTheory.extend_empty

added theorem MeasureTheory.extend_eq

added theorem MeasureTheory.extend_eq_top

added theorem MeasureTheory.extend_iUnion

added theorem MeasureTheory.extend_iUnion_le_tsum_nat'

added theorem MeasureTheory.extend_iUnion_le_tsum_nat

added theorem MeasureTheory.extend_iUnion_nat

added theorem MeasureTheory.extend_mono'

added theorem MeasureTheory.extend_mono

added theorem MeasureTheory.extend_top

added theorem MeasureTheory.extend_union

added def MeasureTheory.inducedOuterMeasure

added theorem MeasureTheory.inducedOuterMeasure_caratheodory

added theorem MeasureTheory.inducedOuterMeasure_eq'

added theorem MeasureTheory.inducedOuterMeasure_eq

added theorem MeasureTheory.inducedOuterMeasure_eq_extend'

added theorem MeasureTheory.inducedOuterMeasure_eq_extend

added theorem MeasureTheory.inducedOuterMeasure_eq_iInf

added theorem MeasureTheory.inducedOuterMeasure_exists_set

added theorem MeasureTheory.inducedOuterMeasure_preimage

added theorem MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter

added theorem MeasureTheory.le_extend

added theorem MeasureTheory.le_inducedOuterMeasure

added theorem MeasureTheory.smul_extend

Created Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

added theorem MeasureTheory.OuterMeasure.biInf_apply'

added theorem MeasureTheory.OuterMeasure.biInf_apply

added def MeasureTheory.OuterMeasure.boundedBy

added theorem MeasureTheory.OuterMeasure.boundedBy_apply

added theorem MeasureTheory.OuterMeasure.boundedBy_eq

added theorem MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction

added theorem MeasureTheory.OuterMeasure.boundedBy_eq_self

added theorem MeasureTheory.OuterMeasure.boundedBy_le

added theorem MeasureTheory.OuterMeasure.boundedBy_top

added theorem MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter

added theorem MeasureTheory.OuterMeasure.boundedBy_zero

added theorem MeasureTheory.OuterMeasure.comap_boundedBy

added theorem MeasureTheory.OuterMeasure.comap_iInf

added theorem MeasureTheory.OuterMeasure.comap_ofFunction

added theorem MeasureTheory.OuterMeasure.iInf_apply'

added theorem MeasureTheory.OuterMeasure.iInf_apply

added theorem MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty

added theorem MeasureTheory.OuterMeasure.isGreatest_ofFunction

added theorem MeasureTheory.OuterMeasure.le_boundedBy'

added theorem MeasureTheory.OuterMeasure.le_boundedBy

added theorem MeasureTheory.OuterMeasure.le_ofFunction

added theorem MeasureTheory.OuterMeasure.map_biInf_comap

added theorem MeasureTheory.OuterMeasure.map_iInf

added theorem MeasureTheory.OuterMeasure.map_iInf_comap

added theorem MeasureTheory.OuterMeasure.map_iInf_le

added theorem MeasureTheory.OuterMeasure.map_ofFunction

added theorem MeasureTheory.OuterMeasure.map_ofFunction_le

added theorem MeasureTheory.OuterMeasure.ofFunction_apply

added theorem MeasureTheory.OuterMeasure.ofFunction_eq

added theorem MeasureTheory.OuterMeasure.ofFunction_eq_sSup

added theorem MeasureTheory.OuterMeasure.ofFunction_le

added theorem MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter

added theorem MeasureTheory.OuterMeasure.restrict_biInf

added theorem MeasureTheory.OuterMeasure.restrict_iInf

added theorem MeasureTheory.OuterMeasure.restrict_iInf_restrict

added theorem MeasureTheory.OuterMeasure.restrict_ofFunction

added theorem MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict

added def MeasureTheory.OuterMeasure.sInfGen

added theorem MeasureTheory.OuterMeasure.sInfGen_def

added theorem MeasureTheory.OuterMeasure.sInf_apply'

added theorem MeasureTheory.OuterMeasure.sInf_apply

added theorem MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen

added theorem MeasureTheory.OuterMeasure.smul_boundedBy

added theorem MeasureTheory.OuterMeasure.smul_ofFunction

Created Mathlib/MeasureTheory/OuterMeasure/Operations.lean

added theorem MeasureTheory.OuterMeasure.add_apply

added def MeasureTheory.OuterMeasure.coeFnAddMonoidHom

added theorem MeasureTheory.OuterMeasure.coe_add

added theorem MeasureTheory.OuterMeasure.coe_bot

added theorem MeasureTheory.OuterMeasure.coe_iSup

added theorem MeasureTheory.OuterMeasure.coe_smul

added theorem MeasureTheory.OuterMeasure.coe_zero

added def MeasureTheory.OuterMeasure.comap

added theorem MeasureTheory.OuterMeasure.comap_apply

added theorem MeasureTheory.OuterMeasure.comap_iSup

added theorem MeasureTheory.OuterMeasure.comap_map

added theorem MeasureTheory.OuterMeasure.comap_mono

added theorem MeasureTheory.OuterMeasure.comap_top

added def MeasureTheory.OuterMeasure.dirac

added theorem MeasureTheory.OuterMeasure.dirac_apply

added theorem MeasureTheory.OuterMeasure.iSup_apply

added theorem MeasureTheory.OuterMeasure.le_comap_map

added def MeasureTheory.OuterMeasure.map

added theorem MeasureTheory.OuterMeasure.map_apply

added theorem MeasureTheory.OuterMeasure.map_comap

added theorem MeasureTheory.OuterMeasure.map_comap_le

added theorem MeasureTheory.OuterMeasure.map_comap_of_surjective

added theorem MeasureTheory.OuterMeasure.map_iSup

added theorem MeasureTheory.OuterMeasure.map_id

added theorem MeasureTheory.OuterMeasure.map_le_restrict_range

added theorem MeasureTheory.OuterMeasure.map_map

added theorem MeasureTheory.OuterMeasure.map_mono

added theorem MeasureTheory.OuterMeasure.map_sup

added theorem MeasureTheory.OuterMeasure.map_top

added theorem MeasureTheory.OuterMeasure.map_top_of_surjective

added theorem MeasureTheory.OuterMeasure.mono''

added def MeasureTheory.OuterMeasure.restrict

added theorem MeasureTheory.OuterMeasure.restrict_apply

added theorem MeasureTheory.OuterMeasure.restrict_empty

added theorem MeasureTheory.OuterMeasure.restrict_iSup

added theorem MeasureTheory.OuterMeasure.restrict_le_self

added theorem MeasureTheory.OuterMeasure.restrict_mono

added theorem MeasureTheory.OuterMeasure.restrict_univ

added theorem MeasureTheory.OuterMeasure.sSup_apply

added theorem MeasureTheory.OuterMeasure.smul_apply

added theorem MeasureTheory.OuterMeasure.smul_dirac_apply

added theorem MeasureTheory.OuterMeasure.smul_iSup

added def MeasureTheory.OuterMeasure.sum

added theorem MeasureTheory.OuterMeasure.sum_apply

added theorem MeasureTheory.OuterMeasure.sup_apply

added theorem MeasureTheory.OuterMeasure.top_apply'

added theorem MeasureTheory.OuterMeasure.top_apply

added theorem MeasureTheory.OuterMeasure.univ_eq_zero_iff

Modified scripts/style-exceptions.txt