AddContent

📁 Source: Mathlib/MeasureTheory/VectorMeasure/AddContent.lean

Statistics

Metric	Count
Definitions AddContent, of_additive_of_le_measure	2
Theorems exists_extension_of_isSetRing_of_le_measure_of_dense, exists_extension_of_isSetSemiring_of_le_measure_of_dense, exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom	3
Total	5

MeasureTheory

Definitions

Name	Category	Theorems
AddContent 📖	CompData	49 math math: sum_addContent_le_of_subset, piContent_tendsto_zero, ProbabilityTheory.Kernel.trajContent_cylinder, AddContent.measure_eq, piContent_cylinder, addContent_diff_of_ne_top, AddContent.extend_eq, projectiveFamilyContent_eq, projectiveFamilyContent_diff, AddContent.isCaratheodory_inducedOuterMeasure_of_mem, ProbabilityTheory.Kernel.trajContent_tendsto_zero, AddContent.supClosure_apply_finpartition, projectiveFamilyContent_cylinder, projectiveFamilyContent_congr, piContent_eq_measure_pi, addContent_sUnion, sum_addContent_eq_of_sUnion_eq, Measure.infinitePiNat_map_piCongrLeft, addContent_mono, addContent_union', projectiveFamilyContent_diff_of_subset, addContent_union, addContent_biUnion_eq, AddContent.inducedOuterMeasure_eq, AddContent.isCaratheodory_inducedOuterMeasure, addContent_eq_add_disjointOfDiffUnion_of_subset, AddContent.ext_iff, addContent_biUnion, addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive, projectiveFamilyContent_iUnion_le, AddContent.extend_eq_top, addContent_sUnion_le_sum, addContent_accumulate, AddContent.supClosure_apply_of_mem, AddContent.measureCaratheodory_eq_inducedOuterMeasure, addContent_iUnion, addContent_biUnion_le, ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj, le_addContent_diff, AddContent.onIoc_apply, projectiveFamilyContent_mono, AddContent.supClosure_apply, eq_add_disjointOfDiff_of_subset, addContent_empty, addContent_le_sum_of_subset_sUnion, AddContent.extend_eq_extend, Measure.piContent_eq_infinitePiNat, addContent_union_le, AddContent.measureCaratheodory_eq

MeasureTheory.VectorMeasure

Definitions

Name	Category	Theorems
of_additive_of_le_measure 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_extension_of_isSetRing_of_le_measure_of_dense 📖	mathematical	MeasureTheory.IsSetRing MeasurableSet ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe MeasureTheory.AddContent ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set MeasureTheory.instFunLikeAddContentSet MeasureTheory.Measure MeasureTheory.Measure.instFunLike Set.instMembership Preorder.toLT symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	measureOf'	—	PseudoEMetricSpace.edist_comm edist_eq_enorm_sub one_mul MeasureTheory.measure_symmDiff_eq MeasurableSet.nullMeasurableSet Set.inter_union_diff MeasureTheory.addContent_union MeasureTheory.IsSetRing.inter_mem MeasureTheory.IsSetRing.diff_mem Disjoint.symm Set.disjoint_sdiff_inter Set.inter_comm add_sub_add_left_eq_sub LE.le.trans enorm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Dense.lipschitzWith_extend isClosed_le OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Continuous.enorm LipschitzWith.continuous MeasureTheory.MeasuredSets.continuous_measure Dense.mono Dense.extend_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IsClosed.closure_eq MeasurableSet.union Nat.instAtLeastTwoHAddOfNat ENNReal.div_pos LT.lt.ne' ENNReal.mul_div_cancel ENNReal.instCharZero LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.disjoint_iff_inter_eq_empty Set.empty_union MeasureTheory.measure_union_le WithTop.add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul MeasureTheory.measure_symmDiff_le sdiff_sdiff_self sdiff_sdiff_right_self sup_of_le_right MeasureTheory.IsSetRing.union_mem Set.union_symmDiff_union_subset Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.termg_eq add_zero one_zsmul Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg enorm_add₄_le Set.disjoint_sdiff_left add_sub_cancel_left sub_self enorm_zero enorm_sub_rev sub_eq_zero enorm_eq_zero sub_add_eq_sub_sub eq_bot_iff le_of_forall_gt ENNReal.instCanonicallyOrderedAdd
exists_extension_of_isSetSemiring_of_le_measure_of_dense 📖	mathematical	MeasureTheory.IsSetSemiring MeasurableSet ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe MeasureTheory.AddContent ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set MeasureTheory.instFunLikeAddContentSet MeasureTheory.Measure MeasureTheory.Measure.instFunLike Set.instMembership ClosureOperator ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike supClosure Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice Preorder.toLT symmDiff SemilatticeSup.toMax Set.instSDiff	measureOf'	—	MeasureTheory.IsSetSemiring.mem_supClosure_iff Finpartition.sup_parts MeasureTheory.AddContent.supClosure_apply_finpartition Finset.sup_set_eq_biUnion MeasureTheory.measure_biUnion_finset Finpartition.disjoint LE.le.trans enorm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Finset.measurableSet_biUnion exists_extension_of_isSetRing_of_le_measure_of_dense MeasureTheory.IsSetSemiring.isSetRing_supClosure subset_supClosure MeasureTheory.AddContent.supClosure_apply_of_mem
exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom 📖	mathematical	MeasureTheory.IsSetSemiring ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm DFunLike.coe MeasureTheory.AddContent ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set MeasureTheory.instFunLikeAddContentSet MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasurableSpace.generateFrom	measureOf'	—	MeasurableSpace.measurableSet_generateFrom MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.exists_ae_subset_biUnion_countable MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasurableSet.sUnion MeasureTheory.isFiniteMeasureRestrict LE.le.trans MeasureTheory.Measure.restrict_apply' MeasureTheory.measure_mono_ae Set.inter_self MeasureTheory.ae_le_set_inter Filter.EventuallyLE.rfl Set.compl_inter_self MeasureTheory.measure_empty MeasureTheory.Measure.restrict_apply_le

---

← Back to Index