OfAddContent

📁 Source: Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean

Statistics

Metric	Count
Definitions measure, measureCaratheodory	2
Theorems inducedOuterMeasure_eq, isCaratheodory_inducedOuterMeasure, isCaratheodory_inducedOuterMeasure_of_mem, isCaratheodory_ofFunction_of_mem, measureCaratheodory_eq, measureCaratheodory_eq_inducedOuterMeasure, measure_eq, ofFunction_eq	8
Total	10

MeasureTheory.AddContent

Definitions

Name	Category	Theorems
measure 📖	CompOp	1 math math: measure_eq
measureCaratheodory 📖	CompOp	2 math math: measureCaratheodory_eq_inducedOuterMeasure, measureCaratheodory_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inducedOuterMeasure_eq 📖	mathematical	MeasureTheory.IsSetSemiring IsSigmaSubadditive Set Set.instMembership	DFunLike.coe MeasureTheory.OuterMeasure ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.inducedOuterMeasure MeasureTheory.AddContent ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty	—	MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty ofFunction_eq extend_eq LE.le.trans_eq extend_eq_top
isCaratheodory_inducedOuterMeasure 📖	mathematical	MeasureTheory.IsSetSemiring MeasurableSet MeasurableSpace.generateFrom	MeasureTheory.OuterMeasure.IsCaratheodory MeasureTheory.inducedOuterMeasure Set Set.instMembership DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty	—	MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty isCaratheodory_inducedOuterMeasure_of_mem MeasureTheory.OuterMeasure.isCaratheodory_empty MeasureTheory.OuterMeasure.isCaratheodory_compl MeasureTheory.OuterMeasure.isCaratheodory_iUnion
isCaratheodory_inducedOuterMeasure_of_mem 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	MeasureTheory.OuterMeasure.IsCaratheodory MeasureTheory.inducedOuterMeasure DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty	—	isCaratheodory_ofFunction_of_mem extend_eq_top
isCaratheodory_ofFunction_of_mem 📖	mathematical	MeasureTheory.IsSetSemiring DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid Set MeasureTheory.instFunLikeAddContentSet Top.top instTopENNReal Set.instMembership	MeasureTheory.OuterMeasure.IsCaratheodory MeasureTheory.OuterMeasure.ofFunction MeasureTheory.addContent_empty	—	MeasureTheory.addContent_empty MeasureTheory.OuterMeasure.isCaratheodory_iff_le' MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem le_iInf MeasureTheory.IsSetSemiring.inter_mem MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff Set.diff_self_inter MeasureTheory.eq_add_disjointOfDiff_of_subset Set.inter_subset_left ENNReal.tsum_add add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add iInf_le_of_le Set.iUnion_inter Set.inter_subset_inter_left le_rfl le_trans MeasureTheory.OuterMeasure.mono Set.diff_subset_diff_left Set.iUnion_diff MeasureTheory.measure_iUnion_le MeasureTheory.OuterMeasure.instOuterMeasureClass instCountableNat ENNReal.tsum_le_tsum Set.sUnion_eq_biUnion Set.iUnion_congr_Prop Finset.sum_congr MeasureTheory.measure_biUnion_finset_le Finset.sum_le_sum MeasureTheory.OuterMeasure.ofFunction_le
measureCaratheodory_eq 📖	mathematical	MeasureTheory.IsSetSemiring IsSigmaSubadditive Set Set.instMembership	DFunLike.coe MeasureTheory.Measure MeasureTheory.OuterMeasure.caratheodory MeasureTheory.inducedOuterMeasure MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty MeasureTheory.Measure.instFunLike measureCaratheodory	—	inducedOuterMeasure_eq
measureCaratheodory_eq_inducedOuterMeasure 📖	mathematical	MeasureTheory.IsSetSemiring IsSigmaSubadditive	DFunLike.coe MeasureTheory.Measure MeasureTheory.OuterMeasure.caratheodory MeasureTheory.inducedOuterMeasure Set Set.instMembership MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty MeasureTheory.Measure.instFunLike measureCaratheodory MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal	—	MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty
measure_eq 📖	mathematical	MeasureTheory.IsSetSemiring MeasurableSpace.generateFrom IsSigmaSubadditive Set Set.instMembership	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike measure Eq.le MeasurableSpace PartialOrder.toPreorder MeasurableSpace.instPartialOrder MeasureTheory.AddContent ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet	—	Eq.le MeasureTheory.IsSetSemiring.empty_mem MeasureTheory.addContent_empty measure.eq_1 MeasureTheory.trim_measurableSet_eq MeasurableSpace.measurableSet_generateFrom measureCaratheodory_eq
ofFunction_eq 📖	mathematical	MeasureTheory.IsSetSemiring IsSigmaSubadditive DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid Set MeasureTheory.instFunLikeAddContentSet Top.top instTopENNReal Set.instMembership	MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal MeasureTheory.OuterMeasure.ofFunction MeasureTheory.addContent_empty	—	le_antisymm MeasureTheory.addContent_empty MeasureTheory.OuterMeasure.ofFunction_le MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem le_iInf Set.inter_eq_self_of_subset_left Set.inter_iUnion MeasureTheory.IsSetSemiring.inter_mem Summable.tsum_le_tsum ENNReal.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional MeasureTheory.addContent_mono ENNReal.instCanonicallyOrderedAdd Set.inter_subset_right ENNReal.summable

---

← Back to Index