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 NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap NNReal.instZero NNReal.instTopologicalSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring instModuleOfContinuousConstSMul Semiring.toModule SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.instFunLike integralLinearMap Real Real.instLE Real.instZero MeasureTheory.integral Real.normedAddCommGroup NormedField.toNormedSpace Real.normedField NNReal.toReal instFunLike UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace 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 IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal partialOrder Real.partialOrder instModuleOfContinuousConstSMul NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul PositiveLinearMap.instFunLike integralPositiveLinearMap MeasureTheory.integral Real.normedAddCommGroup instFunLike	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul

---

← Back to Index