Commit 2023-05-22 18:01 e5bc933f

View on Github →

feat: port MeasureTheory.Measure.Content (#4198)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/Content.lean

added def MeasureTheory.Content.ContentRegular

added theorem MeasureTheory.Content.apply_eq_coe_toFun

added theorem MeasureTheory.Content.borel_le_caratheodory

added theorem MeasureTheory.Content.contentRegular_exists_compact

added theorem MeasureTheory.Content.empty

added def MeasureTheory.Content.innerContent

added theorem MeasureTheory.Content.innerContent_bot

added theorem MeasureTheory.Content.innerContent_comap

added theorem MeasureTheory.Content.innerContent_exists_compact

added theorem MeasureTheory.Content.innerContent_iSup_nat

added theorem MeasureTheory.Content.innerContent_iUnion_nat

added theorem MeasureTheory.Content.innerContent_le

added theorem MeasureTheory.Content.innerContent_mono'

added theorem MeasureTheory.Content.innerContent_mono

added theorem MeasureTheory.Content.innerContent_of_isCompact

added theorem MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant

added theorem MeasureTheory.Content.is_mul_left_invariant_innerContent

added theorem MeasureTheory.Content.is_mul_left_invariant_outerMeasure

added theorem MeasureTheory.Content.le_innerContent

added theorem MeasureTheory.Content.le_outerMeasure_compacts

added theorem MeasureTheory.Content.lt_top

added theorem MeasureTheory.Content.measure_apply

added theorem MeasureTheory.Content.measure_eq_content_of_regular

added theorem MeasureTheory.Content.mono

added theorem MeasureTheory.Content.outerMeasure_caratheodory

added theorem MeasureTheory.Content.outerMeasure_eq_iInf

added theorem MeasureTheory.Content.outerMeasure_exists_compact

added theorem MeasureTheory.Content.outerMeasure_exists_open

added theorem MeasureTheory.Content.outerMeasure_interior_compacts

added theorem MeasureTheory.Content.outerMeasure_le

added theorem MeasureTheory.Content.outerMeasure_lt_top_of_isCompact

added theorem MeasureTheory.Content.outerMeasure_of_isOpen

added theorem MeasureTheory.Content.outerMeasure_opens

added theorem MeasureTheory.Content.outerMeasure_pos_of_is_mul_left_invariant

added theorem MeasureTheory.Content.outerMeasure_preimage

added theorem MeasureTheory.Content.sup_disjoint

added theorem MeasureTheory.Content.sup_le

added structure MeasureTheory.Content