Commit 2023-05-03 11:02 b7bda094

View on Github →

feat: port MeasureTheory.Measure.OuterMeasure (#3674)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Tower.lean

Created Mathlib/MeasureTheory/Measure/OuterMeasure.lean

added def MeasureTheory.OuterMeasure.IsCaratheodory

added theorem MeasureTheory.OuterMeasure.add_apply

added theorem MeasureTheory.OuterMeasure.binfᵢ_apply'

added theorem MeasureTheory.OuterMeasure.binfᵢ_apply

added def MeasureTheory.OuterMeasure.boundedBy

added theorem MeasureTheory.OuterMeasure.boundedBy_apply

added theorem MeasureTheory.OuterMeasure.boundedBy_caratheodory

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_union_of_top_of_nonempty_inter

added theorem MeasureTheory.OuterMeasure.bunionᵢ_null_iff

added def MeasureTheory.OuterMeasure.caratheodoryDynkin

added def MeasureTheory.OuterMeasure.coeFnAddMonoidHom

added theorem MeasureTheory.OuterMeasure.coe_add

added theorem MeasureTheory.OuterMeasure.coe_bot

added theorem MeasureTheory.OuterMeasure.coe_fn_injective

added theorem MeasureTheory.OuterMeasure.coe_smul

added theorem MeasureTheory.OuterMeasure.coe_supᵢ

added theorem MeasureTheory.OuterMeasure.coe_zero

added def MeasureTheory.OuterMeasure.comap

added theorem MeasureTheory.OuterMeasure.comap_apply

added theorem MeasureTheory.OuterMeasure.comap_boundedBy

added theorem MeasureTheory.OuterMeasure.comap_infᵢ

added theorem MeasureTheory.OuterMeasure.comap_map

added theorem MeasureTheory.OuterMeasure.comap_mono

added theorem MeasureTheory.OuterMeasure.comap_ofFunction

added theorem MeasureTheory.OuterMeasure.comap_supᵢ

added theorem MeasureTheory.OuterMeasure.comap_top

added theorem MeasureTheory.OuterMeasure.diff_null

added def MeasureTheory.OuterMeasure.dirac

added theorem MeasureTheory.OuterMeasure.dirac_apply

added theorem MeasureTheory.OuterMeasure.dirac_caratheodory

added theorem MeasureTheory.OuterMeasure.empty'

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.exists_mem_forall_mem_nhds_within_pos

added theorem MeasureTheory.OuterMeasure.ext

added theorem MeasureTheory.OuterMeasure.ext_nonempty

added theorem MeasureTheory.OuterMeasure.f_unionᵢ

added theorem MeasureTheory.OuterMeasure.infᵢ_apply'

added theorem MeasureTheory.OuterMeasure.infᵢ_apply

added def MeasureTheory.OuterMeasure.infₛGen

added theorem MeasureTheory.OuterMeasure.infₛGen_def

added theorem MeasureTheory.OuterMeasure.infₛ_apply'

added theorem MeasureTheory.OuterMeasure.infₛ_apply

added theorem MeasureTheory.OuterMeasure.infₛ_eq_boundedBy_infₛGen

added theorem MeasureTheory.OuterMeasure.isCaratheodory_compl

added theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff

added theorem MeasureTheory.OuterMeasure.isCaratheodory_empty

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.isCaratheodory_unionᵢ_lt

added theorem MeasureTheory.OuterMeasure.isCaratheodory_unionᵢ_nat

added theorem MeasureTheory.OuterMeasure.isGreatest_ofFunction

added theorem MeasureTheory.OuterMeasure.le_add_caratheodory

added theorem MeasureTheory.OuterMeasure.le_boundedBy

added theorem MeasureTheory.OuterMeasure.le_bounded_by'

added theorem MeasureTheory.OuterMeasure.le_comap_map

added theorem MeasureTheory.OuterMeasure.le_inter_add_diff

added theorem MeasureTheory.OuterMeasure.le_ofFunction

added theorem MeasureTheory.OuterMeasure.le_smul_caratheodory

added theorem MeasureTheory.OuterMeasure.le_sum_caratheodory

added theorem MeasureTheory.OuterMeasure.le_trim

added theorem MeasureTheory.OuterMeasure.le_trim_iff

added def MeasureTheory.OuterMeasure.map

added theorem MeasureTheory.OuterMeasure.map_apply

added theorem MeasureTheory.OuterMeasure.map_binfᵢ_comap

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_id

added theorem MeasureTheory.OuterMeasure.map_infᵢ

added theorem MeasureTheory.OuterMeasure.map_infᵢ_comap

added theorem MeasureTheory.OuterMeasure.map_infᵢ_le

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_ofFunction

added theorem MeasureTheory.OuterMeasure.map_ofFunction_le

added theorem MeasureTheory.OuterMeasure.map_sup

added theorem MeasureTheory.OuterMeasure.map_supᵢ

added theorem MeasureTheory.OuterMeasure.map_top

added theorem MeasureTheory.OuterMeasure.map_top_of_surjective

added theorem MeasureTheory.OuterMeasure.measure_inter_union

added theorem MeasureTheory.OuterMeasure.mono''

added theorem MeasureTheory.OuterMeasure.mono'

added theorem MeasureTheory.OuterMeasure.mono_null

added theorem MeasureTheory.OuterMeasure.null_of_locally_null

added theorem MeasureTheory.OuterMeasure.ofFunction_apply

added theorem MeasureTheory.OuterMeasure.ofFunction_caratheodory

added theorem MeasureTheory.OuterMeasure.ofFunction_eq

added theorem MeasureTheory.OuterMeasure.ofFunction_eq_supₛ

added theorem MeasureTheory.OuterMeasure.ofFunction_le

added theorem MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter

added theorem MeasureTheory.OuterMeasure.pos_of_subset_ne_zero

added def MeasureTheory.OuterMeasure.restrict

added theorem MeasureTheory.OuterMeasure.restrict_apply

added theorem MeasureTheory.OuterMeasure.restrict_binfᵢ

added theorem MeasureTheory.OuterMeasure.restrict_empty

added theorem MeasureTheory.OuterMeasure.restrict_infᵢ

added theorem MeasureTheory.OuterMeasure.restrict_infᵢ_restrict

added theorem MeasureTheory.OuterMeasure.restrict_infₛ_eq_infₛ_restrict

added theorem MeasureTheory.OuterMeasure.restrict_le_self

added theorem MeasureTheory.OuterMeasure.restrict_mono

added theorem MeasureTheory.OuterMeasure.restrict_ofFunction

added theorem MeasureTheory.OuterMeasure.restrict_supᵢ

added theorem MeasureTheory.OuterMeasure.restrict_trim

added theorem MeasureTheory.OuterMeasure.restrict_univ

added theorem MeasureTheory.OuterMeasure.smul_apply

added theorem MeasureTheory.OuterMeasure.smul_boundedBy

added theorem MeasureTheory.OuterMeasure.smul_dirac_apply

added theorem MeasureTheory.OuterMeasure.smul_ofFunction

added theorem MeasureTheory.OuterMeasure.smul_supᵢ

added def MeasureTheory.OuterMeasure.sum

added theorem MeasureTheory.OuterMeasure.sum_apply

added theorem MeasureTheory.OuterMeasure.sup_apply

added theorem MeasureTheory.OuterMeasure.supᵢ_apply

added theorem MeasureTheory.OuterMeasure.supᵢ_infₛGen_nonempty

added theorem MeasureTheory.OuterMeasure.supₛ_apply

added theorem MeasureTheory.OuterMeasure.top_apply'

added theorem MeasureTheory.OuterMeasure.top_apply

added theorem MeasureTheory.OuterMeasure.top_caratheodory

added def MeasureTheory.OuterMeasure.trim

added theorem MeasureTheory.OuterMeasure.trim_add

added theorem MeasureTheory.OuterMeasure.trim_binop

added theorem MeasureTheory.OuterMeasure.trim_congr

added theorem MeasureTheory.OuterMeasure.trim_eq

added theorem MeasureTheory.OuterMeasure.trim_eq_infᵢ'

added theorem MeasureTheory.OuterMeasure.trim_eq_infᵢ

added theorem MeasureTheory.OuterMeasure.trim_eq_trim_iff

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_supᵢ

added theorem MeasureTheory.OuterMeasure.trim_trim

added theorem MeasureTheory.OuterMeasure.trim_zero

added theorem MeasureTheory.OuterMeasure.union_null

added theorem MeasureTheory.OuterMeasure.unionᵢ_nat_of_monotone_of_tsum_ne_top

added theorem MeasureTheory.OuterMeasure.unionᵢ_null

added theorem MeasureTheory.OuterMeasure.unionᵢ_null_iff'

added theorem MeasureTheory.OuterMeasure.unionᵢ_null_iff

added theorem MeasureTheory.OuterMeasure.unionᵢ_of_tendsto_zero

added theorem MeasureTheory.OuterMeasure.unionₛ_null_iff

added theorem MeasureTheory.OuterMeasure.univ_eq_zero_iff

added theorem MeasureTheory.OuterMeasure.zero_caratheodory

added structure MeasureTheory.OuterMeasure

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_mono'

added theorem MeasureTheory.extend_mono

added theorem MeasureTheory.extend_union

added theorem MeasureTheory.extend_unionᵢ

added theorem MeasureTheory.extend_unionᵢ_le_tsum_nat'

added theorem MeasureTheory.extend_unionᵢ_le_tsum_nat

added theorem MeasureTheory.extend_unionᵢ_nat

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_infᵢ

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