Content

📁 Source: Mathlib/MeasureTheory/Measure/Content.lean

Statistics

Metric	Count
Definitions Content, ContentRegular, innerContent, instFunLikeCompactsENNReal, measure, outerMeasure, toFun, instInhabitedContent	8
Theorems apply_ne_top, borel_le_caratheodory, contentRegular_exists_compact, empty, innerContent_bot, innerContent_comap, innerContent_exists_compact, innerContent_iSup_nat, innerContent_iUnion_nat, innerContent_le, innerContent_mono, innerContent_mono', innerContent_of_isCompact, innerContent_pos_of_is_add_left_invariant, innerContent_pos_of_is_mul_left_invariant, is_add_left_invariant_innerContent, is_add_left_invariant_outerMeasure, is_mul_left_invariant_innerContent, is_mul_left_invariant_outerMeasure, le_innerContent, le_outerMeasure_compacts, lt_top, measure_apply, measure_eq_content_of_regular, mk_apply, mono, mono', outerMeasure_caratheodory, outerMeasure_eq_iInf, outerMeasure_exists_compact, outerMeasure_exists_open, outerMeasure_interior_compacts, outerMeasure_le, outerMeasure_lt_top_of_isCompact, outerMeasure_of_isOpen, outerMeasure_opens, outerMeasure_pos_of_is_add_left_invariant, outerMeasure_pos_of_is_mul_left_invariant, outerMeasure_preimage, outerRegular, regular, sup_disjoint, sup_disjoint', sup_le, sup_le', toFun_eq_toNNReal_apply	46
Total	54

MeasureTheory

Definitions

Name	Category	Theorems
Content 📖	CompData	22 math math: Content.sup_le, Measure.haar.addHaarContent_apply, Content.le_outerMeasure_compacts, Content.le_innerContent, Content.measure_eq_content_of_regular, Content.lt_top, Content.innerContent_exists_compact, Content.outerMeasure_interior_compacts, Content.mono, Measure.haar.addHaarContent_self, Content.outerMeasure_le, Content.toFun_eq_toNNReal_apply, Measure.haar.haarContent_apply, Measure.haar.haarContent_self, Measure.haar.is_left_invariant_haarContent, Content.mk_apply, Content.empty, Content.innerContent_of_isCompact, Measure.haar.is_left_invariant_addHaarContent, Content.innerContent_le, Content.sup_disjoint, Content.contentRegular_exists_compact
instInhabitedContent 📖	CompOp	—

MeasureTheory.Content

Definitions

Name	Category	Theorems
ContentRegular 📖	MathDef	1 math math: contentRegular_rieszContent
innerContent 📖	CompOp	17 math math: innerContent_mono', le_innerContent, innerContent_iSup_nat, innerContent_exists_compact, is_mul_left_invariant_innerContent, outerMeasure_eq_iInf, innerContent_bot, innerContent_iUnion_nat, outerMeasure_opens, innerContent_pos_of_is_mul_left_invariant, innerContent_of_isCompact, is_add_left_invariant_innerContent, innerContent_pos_of_is_add_left_invariant, innerContent_comap, innerContent_mono, innerContent_le, outerMeasure_of_isOpen
instFunLikeCompactsENNReal 📖	CompOp	22 math math: sup_le, MeasureTheory.Measure.haar.addHaarContent_apply, le_outerMeasure_compacts, le_innerContent, measure_eq_content_of_regular, lt_top, innerContent_exists_compact, outerMeasure_interior_compacts, mono, MeasureTheory.Measure.haar.addHaarContent_self, outerMeasure_le, toFun_eq_toNNReal_apply, MeasureTheory.Measure.haar.haarContent_apply, MeasureTheory.Measure.haar.haarContent_self, MeasureTheory.Measure.haar.is_left_invariant_haarContent, mk_apply, empty, innerContent_of_isCompact, MeasureTheory.Measure.haar.is_left_invariant_addHaarContent, innerContent_le, sup_disjoint, contentRegular_exists_compact
measure 📖	CompOp	7 math math: MeasureTheory.Measure.haarMeasure_apply, measure_eq_content_of_regular, regular, outerRegular, MeasureTheory.Measure.addHaarMeasure_apply, RealRMK.exists_open_approx, measure_apply
outerMeasure 📖	CompOp	23 math math: is_add_left_invariant_outerMeasure, MeasureTheory.Measure.haarMeasure_apply, MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos, le_outerMeasure_compacts, MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos, is_mul_left_invariant_outerMeasure, outerMeasure_preimage, outerMeasure_interior_compacts, outerMeasure_eq_iInf, outerMeasure_le, MeasureTheory.Measure.addHaarMeasure_apply, outerMeasure_pos_of_is_mul_left_invariant, outerMeasure_exists_open, outerMeasure_caratheodory, outerMeasure_exists_compact, borel_le_caratheodory, outerMeasure_opens, outerMeasure_pos_of_is_add_left_invariant, MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos, outerMeasure_lt_top_of_isCompact, MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos, outerMeasure_of_isOpen, measure_apply
toFun 📖	CompOp	4 math math: sup_disjoint', toFun_eq_toNNReal_apply, mono', sup_le'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_ne_top 📖	—	—	—	—	ENNReal.coe_ne_top
borel_le_caratheodory 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE MeasureTheory.OuterMeasure.caratheodory outerMeasure	—	BorelSpace.measurable_eq MeasurableSpace.generateFrom_le outerMeasure_caratheodory IsOpen.inter TopologicalSpace.Opens.isOpen outerMeasure_of_isOpen iSup_subtype' ENNReal.iSup_add Set.empty_subset iSup_le IsCompact.closure TopologicalSpace.Compacts.isCompact le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid mono subset_closure le_refl IsCompact.closure_subset_of_isOpen TopologicalSpace.Compacts.isCompact' TopologicalSpace.Opens.is_open' Set.diff_subset_diff_right add_le_add_right MeasureTheory.measure_mono MeasureTheory.OuterMeasure.instOuterMeasureClass IsOpen.sdiff isClosed_closure ENNReal.add_iSup HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset le_trans ge_of_eq sup_disjoint Disjoint.symm Set.subset_diff le_innerContent
contentRegular_exists_compact 📖	mathematical	ContentRegular	Set Set.instHasSubset TopologicalSpace.Compacts.carrier interior ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts instFunLikeCompactsENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	le_iInf le_of_lt lt_self_iff_false lt_of_le_of_lt' ENNReal.lt_add_right ne_top_of_lt lt_top ENNReal.coe_ne_zero
empty 📖	mathematical	—	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal Bot.bot TopologicalSpace.Compacts.instBot instZeroENNReal	—	sup_of_le_left AddLeftCancelSemigroup.toIsLeftCancelAdd sup_disjoint'
innerContent_bot 📖	mathematical	—	innerContent Bot.bot TopologicalSpace.Opens OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot ENNReal instZeroENNReal	—	le_antisymm empty iSup₂_le TopologicalSpace.Compacts.ext Set.subset_empty_iff TopologicalSpace.Compacts.coe_bot le_refl zero_le ENNReal.instCanonicallyOrderedAdd
innerContent_comap 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.continuous	innerContent FrameHom TopologicalSpace.Opens TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap toContinuousMap Homeomorph.instContinuousMapClass	—	Homeomorph.continuous Function.Surjective.iSup_congr Homeomorph.instContinuousMapClass Equiv.surjective iSup_congr_Prop Set.image_subset_iff
innerContent_exists_compact 📖	mathematical	—	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder innerContent Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Content instFunLikeCompactsENNReal ENNReal.ofNNReal	—	ENNReal.coe_ne_zero le_or_gt Set.empty_subset le_add_left ENNReal.instCanonicallyOrderedAdd ENNReal.sub_lt_self LT.lt.ne_bot innerContent.eq_1 tsub_le_iff_right ENNReal.instOrderedSub le_of_lt
innerContent_iSup_nat 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder innerContent iSup TopologicalSpace.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	Finset.induction_on Finset.sup_empty empty ENNReal.instCanonicallyOrderedAdd Finset.sup_insert Finset.sum_insert le_imp_le_of_le_of_le sup_le le_refl add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid iSup₂_le IsCompact.elim_finite_subcover TopologicalSpace.Compacts.isCompact TopologicalSpace.Opens.isOpen TopologicalSpace.Opens.coe_iSup IsCompact.finite_compact_cover TopologicalSpace.Compacts.ext TopologicalSpace.Compacts.coe_finset_sup Finset.sup_eq_iSup le_trans Finset.sum_le_sum le_iSup ENNReal.sum_le_tsum
innerContent_iUnion_nat 📖	mathematical	IsOpen	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder innerContent Set.iUnion isOpen_iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	innerContent_iSup_nat isOpen_iUnion TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.iSup_def
innerContent_le 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder innerContent DFunLike.coe MeasureTheory.Content instFunLikeCompactsENNReal	—	iSup₂_le mono Set.Subset.trans
innerContent_mono 📖	mathematical	IsOpen Set Set.instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder innerContent	—	biSup_mono HasSubset.Subset.trans Set.instIsTransSubset
innerContent_mono' 📖	mathematical	IsOpen Set Set.instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder innerContent	—	biSup_mono HasSubset.Subset.trans Set.instIsTransSubset
innerContent_of_isCompact 📖	mathematical	IsCompact IsOpen	innerContent DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal	—	le_antisymm iSup₂_le mono le_innerContent Set.Subset.rfl
innerContent_pos_of_is_add_left_invariant 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left IsTopologicalAddGroup.toContinuousAdd Set.Nonempty SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal innerContent	—	continuous_add_left IsTopologicalAddGroup.toContinuousAdd IsOpen.interior_eq TopologicalSpace.Opens.isOpen compact_covered_by_add_left_translates TopologicalSpace.Compacts.isCompact' Homeomorph.instContinuousMapClass isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop TopologicalSpace.Opens.iSup_def LE.le.trans le_innerContent rel_iSup_sum innerContent_bot innerContent_iSup_nat instR1Space IsTopologicalAddGroup.regularSpace Finset.sum_congr is_add_left_invariant_innerContent Finset.sum_const nsmul_eq_mul le_refl ENNReal.mul_pos_iff LT.lt.trans_le Ne.bot_lt
innerContent_pos_of_is_mul_left_invariant 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left IsTopologicalGroup.toContinuousMul Set.Nonempty SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal innerContent	—	continuous_mul_left IsTopologicalGroup.toContinuousMul IsOpen.interior_eq TopologicalSpace.Opens.isOpen compact_covered_by_mul_left_translates TopologicalSpace.Compacts.isCompact' Homeomorph.instContinuousMapClass isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop TopologicalSpace.Opens.iSup_def LE.le.trans le_innerContent rel_iSup_sum innerContent_bot innerContent_iSup_nat instR1Space IsTopologicalGroup.regularSpace Finset.sum_congr is_mul_left_invariant_innerContent Finset.sum_const nsmul_eq_mul ENNReal.mul_pos_iff LT.lt.trans_le Ne.bot_lt
is_add_left_invariant_innerContent 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left	innerContent FrameHom TopologicalSpace.Opens TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap toContinuousMap Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.instContinuousMapClass Homeomorph.addLeft	—	continuous_add_left Homeomorph.instContinuousMapClass innerContent_comap
is_add_left_invariant_outerMeasure 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left	MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure Set.preimage	—	continuous_add_left outerMeasure_preimage
is_mul_left_invariant_innerContent 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left	innerContent FrameHom TopologicalSpace.Opens TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap toContinuousMap Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.instContinuousMapClass Homeomorph.mulLeft	—	continuous_mul_left Homeomorph.instContinuousMapClass innerContent_comap
is_mul_left_invariant_outerMeasure 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left	MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure Set.preimage	—	continuous_mul_left outerMeasure_preimage
le_innerContent 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Content instFunLikeCompactsENNReal innerContent	—	le_iSup_of_le le_iSup
le_outerMeasure_compacts 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts instFunLikeCompactsENNReal MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure SetLike.coe TopologicalSpace.Compacts.instSetLike	—	isOpen_empty innerContent_bot outerMeasure.eq_1 MeasureTheory.inducedOuterMeasure_eq_iInf isOpen_iUnion innerContent_iUnion_nat innerContent_mono le_iInf le_innerContent
lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts instFunLikeCompactsENNReal Top.top instTopENNReal	—	ENNReal.coe_lt_top
measure_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure	—	MeasureTheory.toMeasure_apply borel_le_caratheodory
measure_eq_content_of_regular 📖	mathematical	ContentRegular	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike measure SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike MeasureTheory.Content instFunLikeCompactsENNReal	—	le_antisymm ENNReal.le_of_forall_pos_le_add contentRegular_exists_compact ne_bot_of_gt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass measure_apply IsOpen.measurableSet BorelSpace.opensMeasurable isOpen_interior outerMeasure_interior_compacts IsCompact.closure TopologicalSpace.Compacts.isCompact' mono subset_closure IsClosed.measurableSet isClosed_closure le_outerMeasure_compacts IsCompact.measure_closure
mk_apply 📖	mathematical	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	DFunLike.coe MeasureTheory.Content ENNReal instFunLikeCompactsENNReal ENNReal.ofNNReal	—	—
mono 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Content instFunLikeCompactsENNReal	—	mono'
mono' 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal toFun	—	—
outerMeasure_caratheodory 📖	mathematical	—	MeasurableSet MeasureTheory.OuterMeasure.caratheodory outerMeasure ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal Set.instInter SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike Set.instSDiff	—	TopologicalSpace.Opens.forall MeasureTheory.inducedOuterMeasure_caratheodory isOpen_empty innerContent_bot isOpen_iUnion innerContent_iUnion_nat innerContent_mono'
outerMeasure_eq_iInf 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder IsOpen Set.instHasSubset innerContent	—	MeasureTheory.inducedOuterMeasure_eq_iInf isOpen_empty innerContent_bot isOpen_iUnion innerContent_iUnion_nat innerContent_mono
outerMeasure_exists_compact 📖	mathematical	—	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	outerMeasure_opens innerContent_exists_compact le_imp_le_of_le_of_le le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid le_outerMeasure_compacts
outerMeasure_exists_open 📖	mathematical	—	Set Set.instHasSubset SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal	—	isOpen_empty innerContent_bot MeasureTheory.inducedOuterMeasure_exists_set isOpen_iUnion innerContent_iUnion_nat innerContent_mono ENNReal.coe_ne_zero
outerMeasure_interior_compacts 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure interior SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike MeasureTheory.Content instFunLikeCompactsENNReal	—	LE.le.trans Eq.le outerMeasure_opens innerContent_le interior_subset
outerMeasure_le 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure MeasureTheory.Content instFunLikeCompactsENNReal	—	LE.le.trans Eq.le outerMeasure_opens innerContent_le
outerMeasure_lt_top_of_isCompact 📖	mathematical	IsCompact	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure Top.top instTopENNReal	—	exists_compact_superset MeasureTheory.measure_mono MeasureTheory.OuterMeasure.instOuterMeasureClass outerMeasure_le isOpen_interior interior_subset lt_top
outerMeasure_of_isOpen 📖	mathematical	IsOpen	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure innerContent	—	outerMeasure_opens
outerMeasure_opens 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike innerContent	—	MeasureTheory.inducedOuterMeasure_eq' isOpen_empty innerContent_bot isOpen_iUnion innerContent_iUnion_nat innerContent_mono TopologicalSpace.Opens.is_open'
outerMeasure_pos_of_is_add_left_invariant 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid continuous_add_left IsTopologicalAddGroup.toContinuousAdd IsOpen Set.Nonempty	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure	—	continuous_add_left IsTopologicalAddGroup.toContinuousAdd outerMeasure_opens innerContent_pos_of_is_add_left_invariant
outerMeasure_pos_of_is_mul_left_invariant 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid continuous_mul_left IsTopologicalGroup.toContinuousMul IsOpen Set.Nonempty	Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure	—	continuous_mul_left IsTopologicalGroup.toContinuousMul outerMeasure_opens innerContent_pos_of_is_mul_left_invariant
outerMeasure_preimage 📖	mathematical	DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.map Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.continuous	MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal outerMeasure Set.preimage	—	Homeomorph.continuous MeasureTheory.inducedOuterMeasure_preimage isOpen_empty innerContent_bot isOpen_iUnion innerContent_iUnion_nat innerContent_mono Homeomorph.isOpen_preimage Homeomorph.instContinuousMapClass TopologicalSpace.Opens.is_open' innerContent_comap
outerRegular 📖	mathematical	—	MeasureTheory.Measure.OuterRegular measure	—	outerMeasure_eq_iInf measure_apply IsOpen.measurableSet BorelSpace.opensMeasurable outerMeasure_of_isOpen
regular 📖	mathematical	—	MeasureTheory.Measure.Regular measure	—	LE.le.trans_lt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass subset_closure measure_apply IsClosed.measurableSet BorelSpace.opensMeasurable isClosed_closure outerMeasure_lt_top_of_isCompact IsCompact.closure outerRegular outerMeasure_of_isOpen IsOpen.measurableSet TopologicalSpace.Compacts.isCompact' LT.lt.trans_le LE.le.trans le_outerMeasure_compacts MeasureTheory.le_toMeasure_apply borel_le_caratheodory
sup_disjoint 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	DFunLike.coe MeasureTheory.Content ENNReal instFunLikeCompactsENNReal TopologicalSpace.Compacts.instMax Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Unique.instSubsingleton sup_disjoint'
sup_disjoint' 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe TopologicalSpace.Compacts TopologicalSpace.Compacts.instSetLike	toFun TopologicalSpace.Compacts.instMax NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	—
sup_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts instFunLikeCompactsENNReal TopologicalSpace.Compacts.instMax Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	sup_le'
sup_le' 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal toFun TopologicalSpace.Compacts TopologicalSpace.Compacts.instMax Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	—
toFun_eq_toNNReal_apply 📖	mathematical	—	toFun ENNReal.toNNReal DFunLike.coe MeasureTheory.Content TopologicalSpace.Compacts ENNReal instFunLikeCompactsENNReal	—	—

---

← Back to Index