Documentation Verification Report

Regular

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

Statistics

Metric	Count
Definitions `InnerRegular`, `InnerRegularCompactLTTop`, `InnerRegularWRT`, `OuterRegular`, `Regular`, `WeaklyRegular`	6
Theorems `exists_isOpen_lt_add`, `exists_isOpen_lt_of_lt`, `measure_eq_iInf_isOpen`, `exists_lt_isClosed`, `exists_lt_isCompact`, `measure_eq_iSup_isClosed`, `measure_eq_iSup_isCompact`, `exists_isClosed_diff_lt`, `exists_isClosed_lt_add`, `exists_isCompact_diff_lt`, `exists_isCompact_isClosed_diff_lt`, `exists_isCompact_isClosed_lt_add`, `exists_isCompact_lt_add`, `exists_isOpen_diff_lt`, `exists_isOpen_symmDiff_lt`, `exists_lt_isClosed_of_ne_top`, `exists_lt_isCompact`, `exists_lt_isCompact_of_ne_top`, `measure_eq_iSup_isClosed_of_ne_top`, `measure_eq_iSup_isCompact`, `measure_eq_iSup_isCompact_of_ne_top`, `outerRegular`, `comap`, `comap'`, `exists_isCompact_not_null`, `innerRegular`, `innerRegularWRT_isClosed_isOpen`, `instHAdd`, `instInnerRegularCompactLTTop`, `instSum`, `instSum_1`, `map`, `map_iff`, `map_of_continuous`, `smul`, `smul_nnreal`, `zero`, `innerRegular`, `instInnerRegularOfIsFiniteMeasure`, `instInnerRegularOfSigmaFinite`, `instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure`, `instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure`, `map_of_continuous`, `restrict`, `smul`, `smul_nnreal`, `comap`, `eq_of_innerRegularWRT_of_forall_eq`, `exists_subset_lt_add`, `isCompact_isClosed`, `map`, `map'`, `measurableSet_of_isOpen`, `measure_eq_iSup`, `mono`, `of_imp`, `of_pseudoMetrizableSpace`, `of_restrict`, `of_sigmaFinite`, `restrict`, `restrict_of_measure_ne_top`, `rfl`, `smul`, `trans`, `weaklyRegular_of_finite`, `comap`, `comap'`, `ext_isOpen`, `map`, `measure_closure_eq_of_isCompact`, `of_restrict`, `outerRegular`, `smul`, `smul_nnreal`, `zero`, `comap`, `comap'`, `domSMul`, `exists_isCompact_not_null`, `innerRegular`, `instInnerRegularCompactLTTop`, `map`, `map_iff`, `of_sigmaCompactSpace_of_isLocallyFiniteMeasure`, `restrict_of_measure_ne_top`, `smul`, `smul_nnreal`, `toIsFiniteMeasureOnCompacts`, `toOuterRegular`, `weaklyRegular`, `zero`, `innerRegular`, `innerRegular_measurable`, `of_pseudoMetrizableSpace_of_isFiniteMeasure`, `of_pseudoMetrizableSpace_secondCountable_of_locallyFinite`, `restrict_of_measure_ne_top`, `smul`, `smul_nnreal`, `toOuterRegular`, `zero`, `instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite`, `exists_isOpen_symmDiff_lt`, `exists_isOpen_le_add`, `exists_isOpen_lt_add`, `exists_isOpen_lt_of_lt`, `measure_eq_iInf_isOpen`	106
Total	112

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isOpen_lt_add` 📖	mathematical	`IsCompact`	`Set` `Set.instHasSubset` `IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`exists_isOpen_lt_of_lt` `ENNReal.lt_add_right` `LT.lt.ne` `measure_lt_top` `isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure`
`exists_isOpen_lt_of_lt` 📖	mathematical	`IsCompact` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsOpen`	—	`exists_open_superset_measure_lt_top` `Set.exists_isOpen_lt_of_lt` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `MeasureTheory.Measure.Regular.weaklyRegular` `MeasureTheory.Measure.InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure` `MeasureTheory.Measure.InnerRegularCompactLTTop.restrict` `MeasureTheory.Restrict.isFiniteMeasure` `LE.le.trans_lt` `MeasureTheory.Measure.restrict_apply_le` `Set.subset_inter` `IsOpen.inter` `MeasureTheory.Measure.restrict_apply` `IsOpen.measurableSet` `BorelSpace.opensMeasurable`
`measure_eq_iInf_isOpen` 📖	mathematical	`IsCompact`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `IsOpen`	—	`le_antisymm` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `le_of_forall_gt` `exists_isOpen_lt_of_lt`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_lt_isClosed` 📖	mathematical	`IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsClosed`	—	`MeasureTheory.Measure.WeaklyRegular.innerRegular`
`exists_lt_isCompact` 📖	mathematical	`IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsCompact`	—	`MeasureTheory.Measure.Regular.innerRegular`
`measure_eq_iSup_isClosed` 📖	mathematical	`IsOpen`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `IsClosed`	—	`MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup` `MeasureTheory.Measure.WeaklyRegular.innerRegular`
`measure_eq_iSup_isCompact` 📖	mathematical	`IsOpen`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `IsCompact`	—	`MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup` `MeasureTheory.Measure.Regular.innerRegular`

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isClosed_diff_lt` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsClosed` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instSDiff`	—	`exists_isClosed_lt_add` `MeasureTheory.measure_diff_lt_of_lt_add` `IsClosed.nullMeasurableSet` `ne_top_of_le_ne_top` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`exists_isClosed_lt_add` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsClosed` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add` `MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable` `isClosed_empty`
`exists_isCompact_diff_lt` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsCompact` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instSDiff`	—	`exists_isCompact_lt_add` `MeasureTheory.measure_diff_lt_of_lt_add` `IsCompact.nullMeasurableSet` `ne_top_of_le_ne_top` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`exists_isCompact_isClosed_diff_lt` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsCompact` `IsClosed` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Set.instSDiff`	—	`exists_isCompact_isClosed_lt_add` `MeasureTheory.measure_diff_lt_of_lt_add` `IsClosed.nullMeasurableSet` `BorelSpace.opensMeasurable` `ne_top_of_le_ne_top` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`exists_isCompact_isClosed_lt_add` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsCompact` `IsClosed` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`exists_isCompact_lt_add` `IsCompact.closure_subset_measurableSet` `IsCompact.closure` `isClosed_closure` `IsCompact.measure_closure`
`exists_isCompact_lt_add` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsCompact` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`MeasureTheory.Measure.InnerRegularWRT.exists_subset_lt_add` `MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular` `isCompact_empty`
`exists_isOpen_diff_lt` 📖	mathematical	`MeasurableSet`	`Set` `Set.instHasSubset` `IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `Set.instSDiff`	—	`Set.exists_isOpen_lt_add` `LT.lt.trans_le` `le_top` `MeasureTheory.measure_diff_lt_of_lt_add` `nullMeasurableSet`
`exists_isOpen_symmDiff_lt` 📖	mathematical	`MeasurableSet`	`IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne'` `ENNReal.half_pos` `exists_isCompact_isClosed_diff_lt` `IsCompact.exists_isOpen_lt_add` `LT.lt.trans_le` `le_top` `ENNReal.add_halves` `MeasureTheory.measure_symmDiff_eq` `IsOpen.nullMeasurableSet` `BorelSpace.opensMeasurable` `nullMeasurableSet` `WithTop.add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.diff_subset_diff` `subset_refl` `Set.instReflSubset` `MeasureTheory.measure_diff_lt_of_lt_add` `IsClosed.nullMeasurableSet` `ne_top_of_le_ne_top` `lt_of_le_of_lt`
`exists_lt_isClosed_of_ne_top` 📖	mathematical	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsClosed`	—	`MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable`
`exists_lt_isCompact` 📖	mathematical	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsCompact`	—	`MeasureTheory.Measure.InnerRegular.innerRegular`
`exists_lt_isCompact_of_ne_top` 📖	mathematical	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsCompact`	—	`MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular`
`measure_eq_iSup_isClosed_of_ne_top` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `IsClosed`	—	`MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup` `MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable`
`measure_eq_iSup_isCompact` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `IsCompact`	—	`MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup` `MeasureTheory.Measure.InnerRegular.innerRegular`
`measure_eq_iSup_isCompact_of_ne_top` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset` `IsCompact`	—	`MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup` `MeasureTheory.Measure.InnerRegularCompactLTTop.innerRegular`

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`InnerRegular` 📖	CompData	26 math math: `exists_innerRegular_eq_of_isCompact`, `InnerRegular.instHAdd`, `instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite`, `InnerRegular.map`, `InnerRegular.map_iff`, `InnerRegular.neg`, `InnerRegular.smul`, `InnerRegular.comap'`, `InnerRegular.map_of_continuous`, `MeasureTheory.innerRegular_map_mul_right`, `InnerRegular.comap`, `InnerRegular.inv`, `MeasureTheory.innerRegular_map_smul`, `MeasureTheory.innerRegular_inv_iff`, `MeasureTheory.innerRegular_map_mul_left`, `instInnerRegularOfIsAddHaarMeasureOfCompactSpace`, `MeasureTheory.instInnerRegularOfIsCompletelyPseudoMetrizableSpace`, `MeasureTheory.innerRegular_map_add_left`, `MeasureTheory.innerRegular_map_add_right`, `InnerRegularCompactLTTop.instInnerRegularOfIsFiniteMeasure`, `InnerRegular.smul_nnreal`, `InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite`, `instInnerRegularOfIsHaarMeasureOfCompactSpace`, `MeasureTheory.innerRegular_map_vadd`, `MeasureTheory.innerRegular_neg_iff`, `InnerRegular.zero`
`InnerRegularCompactLTTop` 📖	CompData	7 math math: `MeasureTheory.instInnerRegularCompactLTTopOfIsCompletelyPseudoMetrizableSpace`, `InnerRegularCompactLTTop.restrict`, `Regular.instInnerRegularCompactLTTop`, `InnerRegular.instInnerRegularCompactLTTop`, `InnerRegularCompactLTTop.map_of_continuous`, `InnerRegularCompactLTTop.smul_nnreal`, `InnerRegularCompactLTTop.smul`
`InnerRegularWRT` 📖	MathDef	27 math math: `Regular.innerRegular`, `MeasureTheory.innerRegularWRT_of_exists_compl_lt`, `MeasureTheory.innerRegularWRT_isCompact_isOpen`, `innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group`, `InnerRegularWRT.of_sigmaFinite`, `WeaklyRegular.innerRegular_measurable`, `InnerRegular.innerRegularWRT_isClosed_isOpen`, `InnerRegularWRT.rfl`, `MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure`, `InnerRegularCompactLTTop.innerRegular`, `MeasureTheory.innerRegularWRT_isCompact_isClosed_isOpen`, `MeasureTheory.innerRegularWRT_isCompact_closure_iff`, `MeasureTheory.innerRegularWRT_isCompact_isClosed_iff`, `MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group`, `MeasureTheory.innerRegular_isCompact_isClosed_measurableSet_of_finite`, `InnerRegularWRT.of_imp`, `MeasureTheory.innerRegularWRT_isCompact_closure_of_univ`, `MeasureTheory.innerRegularWRT_isCompact_isClosed`, `MeasureTheory.innerRegularWRT_isCompact`, `MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup`, `innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup`, `MeasureTheory.PolishSpace.innerRegular_isCompact_isClosed_measurableSet`, `InnerRegularWRT.of_pseudoMetrizableSpace`, `InnerRegular.innerRegular`, `WeaklyRegular.innerRegular`, `MeasureTheory.innerRegularWRT_isCompact_closure`, `InnerRegularWRT.isCompact_isClosed`
`OuterRegular` 📖	CompData	10 math math: `OuterRegular.comap`, `WeaklyRegular.toOuterRegular`, `OuterRegular.smul_nnreal`, `OuterRegular.zero`, `MeasureTheory.Content.outerRegular`, `OuterRegular.map`, `OuterRegular.comap'`, `OuterRegular.smul`, `FiniteSpanningSetsIn.outerRegular`, `Regular.toOuterRegular`
`Regular` 📖	CompData	25 math math: `RealRMK.regular_rieszMeasure`, `regular_of_isMulLeftInvariant`, `Regular.inv`, `MeasureTheory.Content.regular`, `regular_addHaarMeasure`, `MeasureTheory.regular_neg_iff`, `Regular.smul`, `Regular.restrict_of_measure_ne_top`, `Regular.comap'`, `Regular.neg`, `Regular.domSMul`, `Regular.of_sigmaCompactSpace_of_isLocallyFiniteMeasure`, `InnerRegularCompactLTTop.instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure`, `exists_regular_eq_of_compactSpace`, `Regular.comap`, `regular_of_isAddLeftInvariant`, `NNRealRMK.rieszMeasure_regular`, `Regular.map`, `regular_haarMeasure`, `Regular.smul_nnreal`, `MeasureTheory.regular_inv_iff`, `instRegularOfIsHaarMeasureOfCompactSpace`, `Regular.map_iff`, `instRegularOfIsAddHaarMeasureOfCompactSpace`, `Regular.zero`
`WeaklyRegular` 📖	CompData	9 math math: `WeaklyRegular.smul_nnreal`, `WeaklyRegular.zero`, `InnerRegularCompactLTTop.instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure`, `Regular.weaklyRegular`, `InnerRegularWRT.weaklyRegular_of_finite`, `WeaklyRegular.of_pseudoMetrizableSpace_of_isFiniteMeasure`, `WeaklyRegular.smul`, `WeaklyRegular.restrict_of_measure_ne_top`, `WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` 📖	mathematical	—	`InnerRegular`	—	`InnerRegularWRT.trans` `InnerRegularWRT.isCompact_isClosed` `InnerRegularWRT.of_restrict` `MeasureTheory.measure_spanningSets_lt_top` `WeaklyRegular.innerRegular_measurable` `WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.Restrict.isFiniteMeasure` `InnerRegularWRT.of_sigmaFinite` `MeasureTheory.Restrict.sigmaFinite` `Eq.superset` `Set.instReflSubset` `MeasureTheory.iUnion_spanningSets` `MeasureTheory.monotone_spanningSets`

MeasureTheory.Measure.FiniteSpanningSetsIn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`outerRegular` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular`	—	`MeasureTheory.Measure.OuterRegular.of_restrict` `set_mem` `Eq.subset` `Set.instReflSubset` `spanning`

MeasureTheory.Measure.InnerRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure.comap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`comap'` `Homeomorph.isOpenEmbedding`
`comap'` 📖	mathematical	`Topology.IsOpenEmbedding`	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure.comap`	—	`MeasureTheory.Measure.InnerRegularWRT.comap` `innerRegular` `Topology.IsOpenEmbedding.measurableEmbedding` `MeasurableEmbedding.measurableSet_image'` `Topology.IsInducing.isCompact_preimage'` `Topology.IsOpenEmbedding.isInducing`
`exists_isCompact_not_null` 📖	mathematical	—	`IsCompact`	—	`MeasurableSet.measure_eq_iSup_isCompact` `MeasurableSet.univ`
`innerRegular` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsCompact` `MeasurableSet`	—	—
`innerRegularWRT_isClosed_isOpen` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsClosed` `IsOpen`	—	`innerRegular` `IsOpen.measurableSet` `IsCompact.closure_subset_of_isOpen` `isClosed_closure` `LT.lt.trans_le` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `subset_closure`
`instHAdd` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure` `MeasureTheory.Measure.instAdd`	—	`eq_or_ne` `MeasurableSet.exists_lt_isCompact` `zero_add` `LT.lt.trans_le` `ENNReal.instCanonicallyOrderedAdd` `add_zero` `ENNReal.exists_lt_add_of_lt_add` `Set.union_subset` `IsCompact.union` `LE.le.trans` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.le` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`instInnerRegularCompactLTTop` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularCompactLTTop`	—	`innerRegular`
`instSum` 📖	mathematical	`MeasureTheory.Measure.InnerRegular`	`Finset.sum` `MeasureTheory.Measure` `MeasureTheory.Measure.instAddCommMonoid`	—	`Finset.induction` `zero` `Finset.sum_insert` `instHAdd`
`instSum_1` 📖	mathematical	`MeasureTheory.Measure.InnerRegular`	`MeasureTheory.Measure.sum`	—	`MeasureTheory.Measure.sum_apply` `Summable.hasSum` `ENNReal.summable` `MeasureTheory.Measure.coe_finset_sum` `Finset.sum_apply` `Filter.Eventually.exists` `Filter.atTop_neBot` `Finset.isDirected_le` `tendsto_order` `ENNReal.instOrderTopology` `MeasurableSet.exists_lt_isCompact` `instSum` `LT.lt.trans_le` `LE.le.trans` `ENNReal.sum_le_tsum` `MeasureTheory.Measure.le_sum_apply`
`map` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`map_of_continuous` `Homeomorph.continuous`
`map_iff` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `Homeomorph.continuous` `Homeomorph.symm_comp_self` `MeasureTheory.Measure.map_id` `map`
`map_of_continuous` 📖	mathematical	`Continuous`	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.InnerRegularWRT.map` `innerRegular` `Continuous.aemeasurable` `BorelSpace.opensMeasurable` `Continuous.measurable` `IsCompact.image`
`smul` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `MeasureTheory.Measure.InnerRegularWRT.smul` `innerRegular`
`smul_nnreal` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`smul`
`zero` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`Set.empty_subset` `isCompact_empty`

MeasureTheory.Measure.InnerRegularCompactLTTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`innerRegular` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsCompact` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	—	—
`instInnerRegularOfIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular`	—	`MeasureTheory.measure_ne_top` `innerRegular`
`instInnerRegularOfSigmaFinite` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegular`	—	`MeasureTheory.Measure.InnerRegularWRT.trans` `innerRegular` `MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite`
`instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.Measure.Regular`	—	`isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure` `MeasureTheory.Measure.InnerRegularWRT.trans` `innerRegular` `MeasureTheory.Measure.InnerRegularWRT.of_imp` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `MeasureTheory.measure_ne_top`
`instWeaklyRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular`	—	`MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite` `MeasureTheory.Measure.InnerRegular.innerRegularWRT_isClosed_isOpen` `BorelSpace.opensMeasurable` `instInnerRegularOfIsFiniteMeasure`
`map_of_continuous` 📖	mathematical	`Continuous`	`MeasureTheory.Measure.InnerRegularCompactLTTop` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.InnerRegularWRT.map` `innerRegular` `Continuous.aemeasurable` `BorelSpace.opensMeasurable` `Continuous.measurable` `MeasureTheory.Measure.map_apply` `IsCompact.image`
`restrict` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularCompactLTTop` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.InnerRegularWRT.restrict` `innerRegular`
`smul` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularCompactLTTop` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `zero_smul` `MeasureTheory.Measure.InnerRegular.instInnerRegularCompactLTTop` `MeasureTheory.Measure.InnerRegular.zero` `MulZeroClass.mul_zero` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.top_mul` `MeasureTheory.Measure.InnerRegularWRT.smul` `innerRegular`
`smul_nnreal` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularCompactLTTop` `NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `smul`

MeasureTheory.Measure.InnerRegularWRT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `MeasurableEmbedding` `Set.image` `Set.preimage`	`MeasureTheory.Measure.comap`	—	`MeasurableEmbedding.comap_apply` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_subset_range` `Function.Injective.preimage_image` `MeasurableEmbedding.injective` `Set.preimage_mono` `Set.image_preimage_eq_iff`
`eq_of_innerRegularWRT_of_forall_eq` 📖	—	`MeasureTheory.Measure.InnerRegularWRT` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—	`measure_eq_iSup` `iSup_congr_Prop`
`exists_subset_lt_add` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `Set` `Set.instEmptyCollection`	`Set.instHasSubset` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`eq_or_ne` `Set.empty_subset` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass` `zero_add` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.sub_lt_self` `ENNReal.lt_add_of_sub_lt_right`
`isCompact_isClosed` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsCompact` `IsClosed`	—	`IsCompact.inter_left` `isCompact_compactCovering` `Set.inter_iUnion` `iUnion_compactCovering` `Set.inter_univ` `Monotone.measure_iUnion` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Monotone.inter` `monotone_const` `Set.monotone_accumulate` `SigmaCompactSpace.exists_compact_covering` `lt_iSup_iff` `Set.inter_subset_left`
`map` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `AEMeasurable` `Set.preimage` `Set.image` `MeasurableSet`	`MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.map_apply_of_aemeasurable` `Set.image_subset_iff` `LT.lt.trans_le` `MeasureTheory.Measure.le_map_apply_image`
`map'` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `Set.preimage` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `Set.image`	`MeasureTheory.Measure.map`	—	`MeasurableEquiv.map_apply` `Set.image_subset_iff` `MeasurableEquiv.preimage_image`
`measurableSet_of_isOpen` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `IsOpen` `Set` `Set.instSDiff`	`MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	—	`LT.lt.trans_le` `LE.le.trans_lt` `bot_le` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_univ` `isOpen_univ` `Set.diff_univ` `Nat.instAtLeastTwoHAddOfNat` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `ENNReal.add_halves` `ENNReal.sub_sub_cancel` `LT.lt.le` `MeasurableSet.exists_isOpen_diff_lt` `Set.exists_isOpen_lt_of_lt` `Set.diff_subset_comm` `exists_subset_lt_add` `LT.lt.ne` `ENNReal.sub_lt_of_lt_add` `MeasureTheory.OuterMeasure.mono` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `tsub_le_iff_right` `MeasureTheory.le_measure_diff` `le_refl` `add_le_add_right` `le_of_lt` `add_assoc`
`measure_eq_iSup` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instHasSubset`	—	`le_antisymm` `le_of_forall_lt` `iSup₂_le` `iSup_le` `MeasureTheory.OuterMeasure.mono`
`mono` 📖	—	`MeasureTheory.Measure.InnerRegularWRT`	—	—	`trans` `of_imp`
`of_imp` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT`	—	`Set.Subset.rfl`
`of_pseudoMetrizableSpace` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsClosed` `IsOpen`	—	`IsOpen.exists_iUnion_isClosed` `lt_iSup_iff` `Monotone.measure_iUnion` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.subset_iUnion`
`of_restrict` 📖	—	`MeasureTheory.Measure.InnerRegularWRT` `MeasureTheory.Measure.restrict` `MeasurableSet` `Set` `Set.instHasSubset` `Set.univ` `Set.iUnion` `Monotone` `Nat.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra`	—	—	`Set.inter_iUnion` `Set.univ_subset_iff` `Set.inter_univ` `Monotone.measure_iUnion` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Monotone.inter` `monotone_const` `lt_iSup_iff` `MeasureTheory.Measure.restrict_apply` `LT.lt.trans_le` `MeasureTheory.Measure.restrict_apply_le`
`of_sigmaFinite` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	—	`Set.inter_iUnion` `MeasureTheory.iUnion_spanningSets` `Set.inter_univ` `Monotone.measure_iUnion` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `PseudoEMetricSpace.pseudoMetrizableSpace` `Monotone.inter` `monotone_const` `MeasureTheory.monotone_spanningSets` `lt_iSup_iff` `Set.inter_subset_left` `MeasurableSet.inter` `MeasureTheory.measurableSet_spanningSets` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_right` `MeasureTheory.measure_spanningSets_lt_top`
`restrict` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	`MeasureTheory.Measure.restrict`	—	`LT.lt.trans_le` `MeasureTheory.Measure.restrict_apply` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.subset_inter` `MeasureTheory.subset_toMeasurable` `Set.inter_subset_left` `MeasurableSet.inter` `MeasureTheory.measurableSet_toMeasurable` `LT.lt.ne` `lt_of_le_of_lt` `MeasureTheory.measure_toMeasurable` `Ne.lt_top` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `MeasureTheory.Measure.restrict_apply'` `Set.inter_eq_left` `MeasureTheory.Measure.restrict_toMeasurable` `MeasureTheory.Measure.le_iff'` `MeasureTheory.Measure.restrict_mono` `le_rfl`
`restrict_of_measure_ne_top` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	`MeasureTheory.Measure.restrict`	—	`Ne.lt_top` `trans` `restrict` `of_imp` `MeasureTheory.measure_ne_top` `MeasureTheory.Restrict.isFiniteMeasure`
`rfl` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT`	—	`Set.Subset.rfl`
`smul` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT`	`ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `ENNReal.mul_iSup` `iSup_congr_Prop` `smul_eq_mul` `measure_eq_iSup` `MeasureTheory.Measure.smul_apply`
`trans` 📖	—	`MeasureTheory.Measure.InnerRegularWRT`	—	—	`HasSubset.Subset.trans` `Set.instIsTransSubset`
`weaklyRegular_of_finite` 📖	mathematical	`MeasureTheory.Measure.InnerRegularWRT` `IsClosed` `IsOpen`	`MeasureTheory.Measure.WeaklyRegular`	—	`MeasureTheory.measure_ne_top` `MeasurableSet.induction_on_open` `exists_subset_lt_add` `isClosed_empty` `Set.Subset.rfl` `LT.lt.le` `le_self_add` `ENNReal.instCanonicallyOrderedAdd` `Set.compl_subset_compl` `IsOpen.isClosed_compl` `IsClosed.isOpen_compl` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `IsClosed.measurableSet` `Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne'` `ENNReal.half_pos` `ENNReal.exists_pos_sum_of_countable'` `instCountableNat` `MeasureTheory.measure_iUnion` `Filter.Tendsto.add` `ENNReal.instContinuousAdd` `Summable.hasSum` `ENNReal.summable` `tendsto_const_nhds` `Filter.Eventually.exists` `Filter.atTop_neBot` `Finset.isDirected_le` `Filter.Tendsto.eventually` `lt_mem_nhds` `ENNReal.instOrderTopology` `ENNReal.lt_add_right` `Set.iUnion_mono` `Set.iUnion_subset` `isClosed_biUnion_finset` `isOpen_iUnion` `LE.le.trans` `Finset.sum_add_distrib` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `Finset.sum_le_sum` `add_le_add_right` `ENNReal.sum_le_tsum` `MeasureTheory.measure_biUnion_finset` `Disjoint.mono` `add_assoc` `ENNReal.add_halves` `MeasureTheory.measure_iUnion_le` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.tsum_le_tsum` `ENNReal.tsum_add` `le_imp_le_of_le_of_le` `le_of_lt` `le_refl` `ENNReal.half_le_self` `exists_between` `ENNReal.instDenselyOrdered` `tsub_pos_iff_lt` `ENNReal.instOrderedSub` `LE.le.trans_lt` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE`

MeasureTheory.Measure.OuterRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular` `MeasureTheory.Measure.comap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`comap'` `Homeomorph.continuous` `Homeomorph.measurableEmbedding`
`comap'` 📖	mathematical	`Continuous` `MeasurableEmbedding`	`MeasureTheory.Measure.OuterRegular` `MeasureTheory.Measure.comap`	—	`outerRegular` `MeasurableEmbedding.measurableSet_image'` `MeasurableEmbedding.comap_apply` `Superset.eq_1` `Set.image_subset_iff` `IsOpen.preimage` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.image_preimage_subset`
`ext_isOpen` 📖	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike`	—	—	`MeasureTheory.Measure.ext` `Set.measure_eq_iInf_isOpen` `iInf_congr_Prop`
`map` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular` `MeasureTheory.Measure.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Set.exists_isOpen_lt_of_lt` `Homeomorph.image_symm` `MeasureTheory.Measure.map_apply` `Homeomorph.measurable` `IsOpen.preimage` `Homeomorph.continuous` `Set.image_subset_iff` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `Homeomorph.preimage_symm` `Homeomorph.preimage_image`
`measure_closure_eq_of_isCompact` 📖	mathematical	`IsCompact`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `closure`	—	`le_antisymm` `Set.measure_eq_iInf_isOpen` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `IsCompact.closure_subset_of_isOpen` `subset_closure`
`of_restrict` 📖	—	`MeasureTheory.Measure.OuterRegular` `MeasureTheory.Measure.restrict` `IsOpen` `Set` `Set.instHasSubset` `Set.univ` `Set.iUnion`	—	—	`lt_of_lt_of_le` `le_top` `IsOpen.measurableSet` `MeasurableSet.inter` `MeasurableSet.disjointed` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_right` `disjointed_subset` `Pairwise.mono` `disjoint_disjointed` `Disjoint.mono` `inf_le_right` `Set.inter_iUnion` `iUnion_disjointed` `Set.univ_subset_iff` `Set.inter_univ` `ENNReal.exists_pos_sum_of_countable'` `LT.lt.ne'` `tsub_pos_iff_lt` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `instCountableNat` `MeasureTheory.Measure.restrict_apply'` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_left` `Set.subset_iUnion` `Set.exists_isOpen_lt_add` `Set.subset_inter` `IsOpen.inter` `Set.inter_eq_self_of_subset_left` `Set.iUnion_mono` `isOpen_iUnion` `MeasureTheory.measure_iUnion_le` `ENNReal.tsum_le_tsum` `LT.lt.le` `ENNReal.tsum_add` `MeasureTheory.measure_iUnion` `add_comm` `lt_tsub_iff_right`
`outerRegular` 📖	mathematical	`MeasurableSet` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`Set.instHasSubset` `IsOpen`	—	—
`smul` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `eq_or_ne` `zero_smul` `zero` `ENNReal.mul_iInf_of_ne` `iInf_congr_Prop` `smul_eq_mul` `Set.measure_eq_iInf_isOpen` `MeasureTheory.Measure.smul_apply`
`smul_nnreal` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular` `NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`smul` `ENNReal.coe_ne_top`
`zero` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`Set.subset_univ` `isOpen_univ`

MeasureTheory.Measure.Regular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `MeasureTheory.Measure.comap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`comap'` `Homeomorph.isOpenEmbedding`
`comap'` 📖	mathematical	`Topology.IsOpenEmbedding`	`MeasureTheory.Measure.Regular` `MeasureTheory.Measure.comap`	—	`MeasureTheory.IsFiniteMeasureOnCompacts.comap'` `toIsFiniteMeasureOnCompacts` `Topology.IsOpenEmbedding.continuous` `Topology.IsOpenEmbedding.measurableEmbedding` `MeasureTheory.Measure.OuterRegular.comap'` `toOuterRegular` `MeasureTheory.Measure.InnerRegularWRT.comap` `innerRegular` `Topology.IsOpenEmbedding.isOpen_iff_image_isOpen` `Topology.IsInducing.isCompact_preimage'` `Topology.IsOpenEmbedding.isInducing`
`domSMul` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `DomMulAct` `MeasureTheory.Measure` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MeasureTheory.Measure.instAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DomMulAct.instMonoidOfMulOpposite` `MulOpposite.instMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MeasureTheory.Measure.instDistribMulActionDomMulAct` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `ContinuousConstSMul.toMeasurableConstSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`map`
`exists_isCompact_not_null` 📖	mathematical	—	`IsCompact`	—	`IsOpen.measure_eq_iSup_isCompact` `isOpen_univ`
`innerRegular` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsCompact` `IsOpen`	—	—
`instInnerRegularCompactLTTop` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularCompactLTTop`	—	`MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen` `toOuterRegular` `innerRegular` `IsCompact.diff`
`map` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `MeasureTheory.Measure.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`MeasureTheory.Measure.IsFiniteMeasureOnCompacts.map` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.OuterRegular.map` `BorelSpace.opensMeasurable` `toOuterRegular` `MeasureTheory.Measure.InnerRegularWRT.map'` `innerRegular` `IsOpen.preimage` `Homeomorph.continuous` `IsCompact.image`
`map_iff` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `MeasureTheory.Measure.map` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`MeasureTheory.Measure.map_map` `Continuous.measurable` `BorelSpace.opensMeasurable` `Homeomorph.continuous` `Homeomorph.symm_comp_self` `MeasureTheory.Measure.map_id` `map`
`of_sigmaCompactSpace_of_isLocallyFiniteMeasure` 📖	mathematical	—	`MeasureTheory.Measure.Regular`	—	`isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `MeasureTheory.Measure.InnerRegularWRT.trans` `MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed` `MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace`
`restrict_of_measure_ne_top` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.WeaklyRegular.restrict_of_measure_ne_top` `weaklyRegular` `MeasureTheory.instIsFiniteMeasureOnCompactsRestrict` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.WeaklyRegular.toOuterRegular` `MeasureTheory.Measure.restrict_apply` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_right` `Ne.lt_top` `MeasurableSet.exists_lt_isCompact_of_ne_top` `MeasureTheory.Measure.InnerRegularCompactLTTop.restrict` `instInnerRegularCompactLTTop`
`smul` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `MeasureTheory.IsFiniteMeasureOnCompacts.smul` `toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.OuterRegular.smul` `toOuterRegular` `MeasureTheory.Measure.InnerRegularWRT.smul` `innerRegular`
`smul_nnreal` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`smul` `ENNReal.coe_ne_top`
`toIsFiniteMeasureOnCompacts` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasureOnCompacts`	—	—
`toOuterRegular` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular`	—	—
`weaklyRegular` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular`	—	`toOuterRegular` `innerRegular` `IsCompact.closure_subset_of_isOpen` `isClosed_closure` `LT.lt.trans_le` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `subset_closure`
`zero` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.isFiniteMeasureZero` `MeasureTheory.Measure.OuterRegular.zero` `Set.empty_subset` `isCompact_empty`

MeasureTheory.Measure.WeaklyRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`innerRegular` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsClosed` `IsOpen`	—	—
`innerRegular_measurable` 📖	mathematical	—	`MeasureTheory.Measure.InnerRegularWRT` `IsClosed` `MeasurableSet` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal`	—	`MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen` `toOuterRegular` `innerRegular` `IsClosed.inter` `IsOpen.isClosed_compl`
`of_pseudoMetrizableSpace_of_isFiniteMeasure` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular`	—	`MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite` `MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace`
`of_pseudoMetrizableSpace_secondCountable_of_locallyFinite` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular`	—	`MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular` `BorelSpace.opensMeasurable` `toOuterRegular` `of_pseudoMetrizableSpace_of_isFiniteMeasure` `MeasureTheory.Restrict.isFiniteMeasure` `MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace`
`restrict_of_measure_ne_top` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular` `MeasureTheory.Measure.restrict`	—	`MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite` `MeasureTheory.Restrict.isFiniteMeasure` `Ne.lt_top` `MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top` `innerRegular_measurable` `IsOpen.measurableSet` `BorelSpace.opensMeasurable`
`smul` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular` `ENNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.right`	—	`IsScalarTower.right` `MeasureTheory.Measure.OuterRegular.smul` `toOuterRegular` `MeasureTheory.Measure.InnerRegularWRT.smul` `innerRegular`
`smul_nnreal` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular` `NNReal` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `Algebra.toSMul` `ENNReal` `instCommSemiringNNReal` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instAlgebraNNReal` `Algebra.id` `IsScalarTower.right`	—	`smul` `ENNReal.coe_ne_top`
`toOuterRegular` 📖	mathematical	—	`MeasureTheory.Measure.OuterRegular`	—	—
`zero` 📖	mathematical	—	`MeasureTheory.Measure.WeaklyRegular` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`MeasureTheory.Measure.OuterRegular.zero` `Set.empty_subset` `isClosed_empty`

MeasureTheory.NullMeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isOpen_symmDiff_lt` 📖	mathematical	`MeasureTheory.NullMeasurableSet`	`IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Top.top` `instTopENNReal` `symmDiff` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Set.instSDiff`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasurableSet.exists_isOpen_symmDiff_lt` `MeasureTheory.measure_congr` `Filter.EventuallyEq.symmDiff` `MeasureTheory.ae_eq_refl`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isOpen_le_add` 📖	mathematical	—	`Set` `instHasSubset` `IsOpen` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`eq_or_ne` `subset_univ` `isOpen_univ` `top_add` `exists_isOpen_lt_add` `LT.lt.le`
`exists_isOpen_lt_add` 📖	mathematical	—	`Set` `instHasSubset` `IsOpen` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`exists_isOpen_lt_of_lt` `ENNReal.lt_add_right`
`exists_isOpen_lt_of_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	`instHasSubset` `IsOpen`	—	`MeasureTheory.Measure.OuterRegular.outerRegular` `MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.measure_toMeasurable` `HasSubset.Subset.trans` `instIsTransSubset` `MeasureTheory.subset_toMeasurable`
`measure_eq_iInf_isOpen` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `instHasSubset` `IsOpen`	—	`le_antisymm` `le_iInf₂` `le_iInf` `MeasureTheory.OuterMeasure.mono` `le_of_forall_gt` `exists_isOpen_lt_of_lt`

---

← Back to Index