CompactlySupported

📁 Source: Mathlib/MeasureTheory/Integral/CompactlySupported.lean

Statistics

Metric	Count
Definitions integralLinearMap, integralPositiveLinearMap	2
Theorems integrable, integralLinearMap_apply, integralPositiveLinearMap_toFun	3
Total	5

CompactlySupportedContinuousMap

Definitions

Name	Category	Theorems
integralLinearMap 📖	CompOp	4 math math: NNRealRMK.integralLinearMap_inj, NNRealRMK.integralLinearMap_rieszMeasure, integralLinearMap_apply, NNRealRMK.rieszMeasure_integralLinearMap
integralPositiveLinearMap 📖	CompOp	5 math math: RealRMK.rieszMeasure_integralPositiveLinearMap, RealRMK.integralPositiveLinearMap_inj, integralLinearMap_apply, RealRMK.integralPositiveLinearMap_rieszMeasure, integralPositiveLinearMap_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integrable 📖	mathematical	—	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup instFunLike	—	Continuous.integrable_of_hasCompactSupport ContinuousMap.continuous hasCompactSupport
integralLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap NNReal instSemiringNNReal RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap instZeroNNReal NNReal.instTopologicalSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring instModuleOfContinuousConstSMul Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul LinearMap.instFunLike integralLinearMap Real Real.instLE Real.instZero MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField NNReal.toReal instFunLike UniformSpace.toTopologicalSpace Real.pseudoMetricSpace toReal integralPositiveLinearMap toReal_apply	—	toReal_apply
integralPositiveLinearMap_toFun 📖	mathematical	—	DFunLike.coe PositiveLinearMap Real CompactlySupportedContinuousMap Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring instAddCommMonoidOfContinuousAdd Real.instAddCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal partialOrder Real.partialOrder 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 integralPositiveLinearMap MeasureTheory.integral Real.normedAddCommGroup instFunLike	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul

---

← Back to Index