Documentation Verification Report

Real

📁 Source: Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean

Statistics

Metric	Count
Definitions `rieszMeasure`	1
Theorems `exists_innerRegular_eq_of_isCompact`, `exists_regular_eq_of_compactSpace`, `ext_of_integral_eq_on_compactlySupported`, `exists_open_approx`, `instIsFiniteMeasureRieszMeasure`, `integralPositiveLinearMap_inj`, `integralPositiveLinearMap_rieszMeasure`, `integral_rieszMeasure`, `le_rieszMeasure_tsupport_subset`, `measure_le_of_isCompact_of_integral`, `range_cut_partition`, `regular_rieszMeasure`, `rieszMeasure_integralPositiveLinearMap`, `rieszMeasure_le_of_eq_one`	14
Total	15

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_innerRegular_eq_of_isCompact` 📖	mathematical	`IsCompact` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Compl.compl` `Set.instCompl` `instZeroENNReal`	`InnerRegular` `MeasureTheory.IsFiniteMeasure` `MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike`	—	`isCompact_iff_compactSpace` `exists_regular_eq_of_compactSpace` `instT2SpaceSubtype` `Subtype.borelSpace` `MeasureTheory.IsFiniteMeasure_comap` `InnerRegular.map_of_continuous` `InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite` `Regular.instInnerRegularCompactLTTop` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `continuous_subtype_val` `isFiniteMeasure_map` `map_apply` `Measurable.subtype_coe` `measurable_id'` `MeasurableSet.compl` `IsCompact.measurableSet` `BorelSpace.opensMeasurable` `Subtype.coe_preimage_self` `Set.compl_univ` `MeasureTheory.measure_empty` `instOuterMeasureClass` `MeasureTheory.integral_map` `Measurable.aemeasurable` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `BoundedContinuousFunction.instBoundedContinuousMapClass` `map_comap_subtype_coe` `restrict_eq_self_of_ae_mem`
`exists_regular_eq_of_compactSpace` 📖	mathematical	—	`Regular` `MeasureTheory.IsFiniteMeasure` `MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `BoundedContinuousFunction.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `MeasureTheory.integral_add` `CompactlySupportedContinuousMap.integrable` `BorelSpace.opensMeasurable` `isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.integral_smul` `NormedSpace.toNormSMulClass` `Algebra.to_smulCommClass` `MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `T3Space.toRegularSpace` `T4Space.t3Space` `T4Space.of_paracompactSpace_t2Space` `paracompact_of_locallyCompact_sigmaCompact` `instWeaklyLocallyCompactSpaceOfCompactSpace` `CompactSpace.sigmaCompact` `RealRMK.regular_rieszMeasure` `RealRMK.instIsFiniteMeasureRieszMeasure` `ContinuousMapClass.map_continuous` `BoundedContinuousMapClass.toContinuousMapClass` `BoundedContinuousFunction.instBoundedContinuousMapClass` `HasCompactSupport.of_compactSpace` `RealRMK.integral_rieszMeasure`
`ext_of_integral_eq_on_compactlySupported` 📖	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `DFunLike.coe` `CompactlySupportedContinuousMap` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike`	—	—	`OuterRegular.ext_isOpen` `WeaklyRegular.toOuterRegular` `Regular.weaklyRegular` `T2Space.r1Space` `InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eq` `Regular.innerRegular` `le_antisymm` `RealRMK.measure_le_of_isCompact_of_integral` `Regular.toIsFiniteMeasureOnCompacts` `Eq.le` `Eq.ge`

RealRMK

Definitions

Name	Category	Theorems
`rieszMeasure` 📖	CompOp	7 math math: `rieszMeasure_integralPositiveLinearMap`, `instIsFiniteMeasureRieszMeasure`, `regular_rieszMeasure`, `rieszMeasure_le_of_eq_one`, `integral_rieszMeasure`, `integralPositiveLinearMap_rieszMeasure`, `le_rieszMeasure_tsupport_subset`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_open_approx` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `MeasurableSet` `DFunLike.coe` `CompactlySupportedContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike`	`Set` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Content.measure` `T2Space.r1Space` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofReal`	—	`ne_of_gt` `Real.toNNReal_pos` `T2Space.r1Space` `MeasureTheory.Content.outerMeasure_exists_open` `IsOpen.preimage` `ContinuousMap.continuous_toFun` `isOpen_Iio` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Set.subset_inter` `Set.mem_of_mem_inter_right` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Content.measure_apply` `IsOpen.measurableSet` `BorelSpace.opensMeasurable` `TopologicalSpace.Opens.is_open'` `ENNReal.ofNNReal_toNNReal`
`instIsFiniteMeasureRieszMeasure` 📖	mathematical	—	`MeasureTheory.IsFiniteMeasure` `rieszMeasure` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `T3Space.toRegularSpace` `T4Space.t3Space` `T4Space.of_paracompactSpace_t2Space` `paracompact_of_locallyCompact_sigmaCompact` `instWeaklyLocallyCompactSpaceOfCompactSpace` `CompactSpace.sigmaCompact`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `WeaklyLocallyCompactSpace.locallyCompactSpace` `instR1Space` `T3Space.toRegularSpace` `T4Space.t3Space` `T4Space.of_paracompactSpace_t2Space` `paracompact_of_locallyCompact_sigmaCompact` `instWeaklyLocallyCompactSpaceOfCompactSpace` `CompactSpace.sigmaCompact` `HasCompactSupport.of_compactSpace` `rieszMeasure_le_of_eq_one` `zero_le_one` `Real.instZeroLEOneClass` `isCompact_univ`
`integralPositiveLinearMap_inj` 📖	mathematical	—	`CompactlySupportedContinuousMap.integralPositiveLinearMap` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported`
`integralPositiveLinearMap_rieszMeasure` 📖	mathematical	—	`CompactlySupportedContinuousMap.integralPositiveLinearMap` `BorelSpace.opensMeasurable` `rieszMeasure` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `regular_rieszMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `PositiveLinearMap.ext` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `regular_rieszMeasure` `integral_rieszMeasure`
`integral_rieszMeasure` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `rieszMeasure` `DFunLike.coe` `CompactlySupportedContinuousMap` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `PositiveLinearMap` `Real.semiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `Real.instAddCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PositiveLinearMap.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `le_antisymm` `instIsTopologicalAddGroupReal` `neg_neg` `MeasureTheory.integral_neg'` `neg_le_neg` `Real.instIsOrderedAddMonoid` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `PositiveLinearMap.instLinearMapClass`
`le_rieszMeasure_tsupport_subset` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `CompactlySupportedContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `Real.instOne` `Set` `Set.instHasSubset` `tsupport`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal` `PositiveLinearMap` `Real.semiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `Real.instAddCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PositiveLinearMap.instFunLike` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `rieszMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `le_trans` `T2Space.r1Space` `CompactlySupportedContinuousMap.hasCompactSupport` `MeasureTheory.Content.measure_eq_content_of_regular` `contentRegular_rieszContent` `rieszMeasure.eq_1` `rieszContentAux_mono` `rieszContentAux_union` `rieszContentAux_sup_le` `rieszContent.eq_1` `PositiveLinearMap.map_nonneg` `ENNReal.ofReal_eq_coe_nnreal` `MeasureTheory.Content.mk_apply` `ENNReal.coe_le_coe` `le_iff_forall_pos_le_add` `NNReal.instDenselyOrdered` `CanonicallyOrderedAdd.toExistsAddOfLE` `NNReal.instCanonicallyOrderedAdd` `NNReal.addLeftReflectLT` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftMono` `NNReal.instIsTopologicalSemiring` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `exists_lt_rieszContentAux_add_pos` `Real.toNNReal_pos` `LE.le.trans` `OrderHom.mono` `CompactlySupportedContinuousMap.toReal_apply` `Real.toNNReal_coe` `image_eq_zero_of_notMem_tsupport` `LT.lt.le` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`measure_le_of_isCompact_of_integral` 📖	mathematical	`Real` `Real.instLE` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `DFunLike.coe` `CompactlySupportedContinuousMap` `Real.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `IsCompact`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`ENNReal.le_of_forall_pos_le_add` `LT.lt.ne` `IsCompact.measure_lt_top` `Set.exists_isOpen_le_add` `ne_of_gt` `ENNReal.coe_lt_coe` `LE.le.trans_lt` `Ne.lt_top` `ENNReal.Finiteness.add_ne_top` `ENNReal.coe_ne_top` `exists_continuousMap_one_of_isCompact_subset_isOpen` `T2Space.r1Space` `hasCompactSupport_def` `Set.indicator_of_mem` `image_eq_zero_of_notMem_tsupport` `Real.instZeroLEOneClass` `Set.indicator_of_notMem` `MeasureTheory.integral_indicator_one` `IsCompact.measurableSet` `BorelSpace.opensMeasurable` `MeasureTheory.integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `MeasureTheory.IntegrableOn.integrable_indicator` `ContinuousOn.integrableOn_compact` `continuousOn_const` `CompactlySupportedContinuousMap.integrable` `MeasureTheory.integrableOn_const` `ne_top_of_lt` `enorm_ne_top` `IsOpen.measurableSet` `MeasureTheory.measureReal_def` `ENNReal.coe_toReal` `ENNReal.toReal_add` `ENNReal.toReal_le_toReal`
`range_cut_partition` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instHasSubset` `Set.range` `DFunLike.coe` `CompactlySupportedContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `Set.Ioo` `Real.instPreorder` `Real.instAdd` `Real.instMul` `Real.instNatCast`	`tsupport` `Set.iUnion` `Set.PairwiseDisjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.univ` `Real.instLE` `Real.instOne` `MeasurableSet`	—	`add_le_add_three` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_refl` `mul_le_mul_iff_of_pos_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_one` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `mul_add` `Distrib.leftDistribClass` `mul_one` `add_assoc` `CharP.cast_eq_zero` `CharP.ofCharZero` `MulZeroClass.zero_mul` `add_zero` `Set.Ioo_subset_Ioc_self` `Ioc_subset_biUnion_Ioc` `Set.iUnion_congr_Prop` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_comm` `Nat.cast_add` `Set.mem_range_self` `Disjoint.preimage` `le_trans` `Set.mem_setOf_eq` `le_tsub_of_add_le_right` `AddGroup.toOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `lt_of_le_of_lt` `le_of_not_gt` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `MeasurableSet.inter` `ContinuousMap.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `measurableSet_Ioc` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `measurableSet_closure`
`regular_rieszMeasure` 📖	mathematical	—	`MeasureTheory.Measure.Regular` `rieszMeasure`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `MeasureTheory.Content.regular` `T2Space.r1Space` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace`
`rieszMeasure_integralPositiveLinearMap` 📖	mathematical	—	`rieszMeasure` `CompactlySupportedContinuousMap.integralPositiveLinearMap` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts`	—	`MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported` `BorelSpace.opensMeasurable` `MeasureTheory.Measure.Regular.toIsFiniteMeasureOnCompacts` `regular_rieszMeasure` `integral_rieszMeasure`
`rieszMeasure_le_of_eq_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `CompactlySupportedContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `CompactlySupportedContinuousMap.instFunLike` `IsCompact` `Real.instOne`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `rieszMeasure` `ENNReal.ofReal` `PositiveLinearMap` `Real.semiring` `CompactlySupportedContinuousMap.instAddCommMonoidOfContinuousAdd` `Real.instAddCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `CompactlySupportedContinuousMap.partialOrder` `Real.partialOrder` `CompactlySupportedContinuousMap.instModuleOfContinuousConstSMul` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedSpace` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `Real.instRing` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `PositiveLinearMap.instFunLike`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `T2Space.r1Space` `rieszMeasure.eq_1` `MeasureTheory.Content.measure_eq_content_of_regular` `contentRegular_rieszContent` `ENNReal.coe_le_iff` `csInf_le'` `Set.mem_image` `Eq.ge` `NNReal.eq` `NNReal.instIsTopologicalSemiring` `IsBoundedSMul.toUniformContinuousConstSMul` `NNReal.isBoundedSMul` `CompactlySupportedContinuousMap.toNNRealLinear_apply` `CompactlySupportedContinuousMap.ext` `CompactlySupportedContinuousMap.toReal_apply` `sup_of_le_left` `ENNReal.ofReal_eq_ofReal_iff` `PositiveLinearMap.map_nonneg` `NNReal.zero_le_coe` `ENNReal.ofReal_coe_nnreal`

---

← Back to Index