CompactlySupported

📁 Source: Mathlib/Topology/ContinuousMap/CompactlySupported.lean

Statistics

Metric	Count
Definitions «termC_c(_,_)»»), «term_→C_c_», CompactlySupportedContinuousMap, liftCompactlySupported, coeFnMonoidHom, comp, compAddMonoidHom, compLeft, compLinearMap, compMulHom, compNonUnitalAlgHom, continuousMapEquiv, copy, instAddCommGroupOfIsTopologicalAddGroup, instAddCommMonoidOfContinuousAdd, instAddGroup, instAddMonoidOfContinuousAdd, instAddOfContinuousAdd, instAddZeroClassOfContinuousAdd, instFunLike, instInf, instInhabited, instLatticeOfTopologicalLattice, instModuleOfContinuousConstSMul, instMulActionWithZeroOfContinuousConstSMul, instMulOfContinuousMul, instMulZeroClassOfContinuousMul, instNeg, instNonUnitalCommRingOfIsTopologicalRing, instNonUnitalCommSemiringOfIsTopologicalSemiring, instNonUnitalNonAssocRingOfIsTopologicalRing, instNonUnitalNonAssocSemiringOfIsTopologicalSemiring, instNonUnitalRingOfIsTopologicalRing, instNonUnitalSemiringOfIsTopologicalSemiring, instSMulOfContinuousConstSMul, instSMulOfContinuousSMulOfContinuousMapClass, instSMulWithZeroOfContinuousConstSMul, instSemigroupWithZeroOfContinuousMul, instStar, instStarAddMonoid, instStarRing, instSub, instSup, instZero, nnrealPart, partialOrder, pullback_addMonoidHom, pullback_monoidHom, semilatticeInf, semilatticeSup, toBoundedContinuousFunction, toContinuousMap, toNNRealLinear, toReal, toRealLinearMap, toRealPositiveLinear, CompactlySupportedContinuousMapClass, instCoeTCCompactlySupportedContinuousMap	58
Theorems add_apply, coe_add, coe_compLeft, coe_comp_to_continuous_fun, coe_copy, coe_finsetInf', coe_finsetSup', coe_inf, coe_mk, coe_mul, coe_neg, coe_smul, coe_smulc, coe_star, coe_sub, coe_sum, coe_sup, coe_toContinuousMap, coe_toRealLinearMap, coe_zero, compLeft_apply, comp_assoc, comp_id, continuousMapEquiv_apply_toFun, continuousMapEquiv_symm_apply, copy_eq, eq_of_empty, eq_toNNRealLinear_toRealPositiveLinear, eq_toRealPositiveLinear_toReal, exists_add_nnrealPart_add_eq, exists_add_of_le, ext, ext_iff, finsetInf'_apply, finsetSup'_apply, hasCompactSupport, hasCompactSupport', inf_apply, instAddLeftMono, instAddRightMono, instCompactlySupportedContinuousMapClass, instIsCentralScalar, instIsOrderedAddMonoid, instIsScalarTower, instMulLeftMono, instMulRightMono, instSMulCommClass, instStarModule, instTrivialStar, le_def, lt_def, mul_apply, neg_apply, nnrealPart_add_le_add_nnrealPart, nnrealPart_apply, nnrealPart_neg_eq_zero_of_nonneg, nnrealPart_neg_toReal_eq, nnrealPart_smul_neg, nnrealPart_smul_pos, nnrealPart_sub_nnrealPart_neg, nnrealPart_toReal_eq, pullback_addMonoidHom_def, pullback_monoidHom_def, smul_apply, smulc_apply, star_apply, sub_apply, sum_apply, sup_apply, toBoundedContinuousFunction_apply, toContinuousMap_compLeft, toNNRealLinear_apply, toNNRealLinear_inj, toRealLinearMap_apply, toRealLinearMap_apply_apply, toRealPositiveLinear_apply, toReal_add, toReal_apply, toReal_nonneg, toReal_smul, zero_apply, zero_comp, hasCompactSupport, instZeroAtInftyContinuousMapClass, of_compactSpace, toContinuousMapClass, uniformContinuous	87
Total	145

CompactlySupported

Definitions

Name	Category	Theorems
«termC_c(_,_)» 📖» "API Documentation")	CompOp	—
«term_→C_c_» 📖	CompOp	—

CompactlySupportedContinuousMap

Definitions

Name	Category	Theorems
coeFnMonoidHom 📖	CompOp	—
comp 📖	CompOp	4 math math: zero_comp, comp_id, coe_comp_to_continuous_fun, comp_assoc
compAddMonoidHom 📖	CompOp	—
compLeft 📖	CompOp	3 math math: toContinuousMap_compLeft, compLeft_apply, coe_compLeft
compLinearMap 📖	CompOp	—
compMulHom 📖	CompOp	—
compNonUnitalAlgHom 📖	CompOp	—
continuousMapEquiv 📖	CompOp	2 math math: continuousMapEquiv_symm_apply, continuousMapEquiv_apply_toFun
copy 📖	CompOp	2 math math: coe_copy, copy_eq
instAddCommGroupOfIsTopologicalAddGroup 📖	CompOp	—
instAddCommMonoidOfContinuousAdd 📖	CompOp	34 math math: TopologicalGroup.IsSES.integral_inducedMeasure, TopologicalGroup.IsSES.pushforward_def, NNRealRMK.lintegral_rieszMeasure, toRealLinearMap_apply_apply, rieszContentAux_image_nonempty, TopologicalAddGroup.IsSES.pushforward_apply_apply, coe_toRealLinearMap, RealRMK.rieszMeasure_le_of_eq_one, toRealLinearMap_apply, RealRMK.integral_rieszMeasure, toRealPositiveLinear_apply, integralLinearMap_apply, TopologicalGroup.IsSES.integrate_apply, TopologicalAddGroup.IsSES.integrate_mono, TopologicalGroup.IsSES.pushforward_apply_apply, instIsOrderedAddMonoid, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, toNNRealLinear_apply, TopologicalAddGroup.IsSES.pushforward_def, NNRealRMK.le_rieszMeasure_of_tsupport_subset, sum_apply, exists_lt_rieszContentAux_add_pos, TopologicalGroup.IsSES.pushforward_mono, TopologicalAddGroup.IsSES.integral_inducedMeasure, TopologicalAddGroup.IsSES.pushforward_mono, eq_toRealPositiveLinear_toReal, integralPositiveLinearMap_toFun, NNRealRMK.integral_rieszMeasure, monotone_of_nnreal, RealRMK.le_rieszMeasure_tsupport_subset, TopologicalGroup.IsSES.integrate_mono, coe_sum, TopologicalAddGroup.IsSES.integrate_apply, rieszContentAux_le
instAddGroup 📖	CompOp	—
instAddMonoidOfContinuousAdd 📖	CompOp	—
instAddOfContinuousAdd 📖	CompOp	9 math math: instAddRightMono, exists_add_of_le, nnrealPart_add_le_add_nnrealPart, add_apply, toReal_add, coe_add, instAddLeftMono, exists_continuous_add_one_of_isCompact_nnreal, exists_add_nnrealPart_add_eq
instAddZeroClassOfContinuousAdd 📖	CompOp	—
instFunLike 📖	CompOp	70 math math: coe_mk, coe_sub, coe_inf, coe_mul, TopologicalGroup.IsSES.integral_inducedMeasure, hasCompactSupport, toBoundedContinuousFunction_apply, TopologicalGroup.IsSES.integral_pullback_invFun_apply, TopologicalGroup.IsSES.pullback_def, TopologicalGroup.IsSES.pushforward_def, star_apply, sub_apply, NNRealRMK.lintegral_rieszMeasure, toRealLinearMap_apply_apply, coe_star, mul_apply, TopologicalAddGroup.IsSES.pushforward_apply_apply, smul_apply, instCompactlySupportedContinuousMapClass, instSMulCommClass, coe_smul, RealRMK.integral_rieszMeasure, integrable, toContinuousMap_compLeft, smulc_apply, sup_apply, toReal_apply, pullback_addMonoidHom_def, compLeft_apply, integralLinearMap_apply, TopologicalGroup.IsSES.integrate_apply, le_def, ext_iff, coe_compLeft, coe_copy, TopologicalGroup.IsSES.pushforward_apply_apply, TopologicalAddGroup.IsSES.integral_pullback_invFun_apply, finsetInf'_apply, inf_apply, add_apply, coe_zero, coe_sup, zero_apply, TopologicalAddGroup.IsSES.pushforward_def, coe_toContinuousMap, coe_smulc, sum_apply, RealRMK.exists_open_approx, exists_lt_rieszContentAux_add_pos, coe_comp_to_continuous_fun, continuousMapEquiv_symm_apply, lt_def, TopologicalAddGroup.IsSES.integral_inducedMeasure, coe_finsetInf', neg_apply, nnrealPart_apply, integralPositiveLinearMap_toFun, coe_neg, coe_add, TopologicalAddGroup.IsSES.pullback_def, coe_finsetSup', RealRMK.range_cut_partition, NNRealRMK.integral_rieszMeasure, exists_continuous_add_one_of_isCompact_nnreal, pullback_monoidHom_def, instIsScalarTower, finsetSup'_apply, coe_sum, TopologicalAddGroup.IsSES.integrate_apply, continuousMapEquiv_apply_toFun
instInf 📖	CompOp	2 math math: coe_inf, inf_apply
instInhabited 📖	CompOp	—
instLatticeOfTopologicalLattice 📖	CompOp	—
instModuleOfContinuousConstSMul 📖	CompOp	31 math math: TopologicalGroup.IsSES.integral_inducedMeasure, TopologicalGroup.IsSES.pushforward_def, NNRealRMK.lintegral_rieszMeasure, toRealLinearMap_apply_apply, rieszContentAux_image_nonempty, TopologicalAddGroup.IsSES.pushforward_apply_apply, coe_toRealLinearMap, RealRMK.rieszMeasure_le_of_eq_one, toRealLinearMap_apply, RealRMK.integral_rieszMeasure, toRealPositiveLinear_apply, integralLinearMap_apply, TopologicalGroup.IsSES.integrate_apply, TopologicalAddGroup.IsSES.integrate_mono, TopologicalGroup.IsSES.pushforward_apply_apply, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, toNNRealLinear_apply, TopologicalAddGroup.IsSES.pushforward_def, NNRealRMK.le_rieszMeasure_of_tsupport_subset, exists_lt_rieszContentAux_add_pos, TopologicalGroup.IsSES.pushforward_mono, TopologicalAddGroup.IsSES.integral_inducedMeasure, TopologicalAddGroup.IsSES.pushforward_mono, eq_toRealPositiveLinear_toReal, integralPositiveLinearMap_toFun, NNRealRMK.integral_rieszMeasure, monotone_of_nnreal, RealRMK.le_rieszMeasure_tsupport_subset, TopologicalGroup.IsSES.integrate_mono, TopologicalAddGroup.IsSES.integrate_apply, rieszContentAux_le
instMulActionWithZeroOfContinuousConstSMul 📖	CompOp	—
instMulOfContinuousMul 📖	CompOp	4 math math: coe_mul, mul_apply, instMulRightMono, instMulLeftMono
instMulZeroClassOfContinuousMul 📖	CompOp	—
instNeg 📖	CompOp	8 math math: nnrealPart_smul_neg, nnrealPart_neg_toReal_eq, toRealPositiveLinear_apply, neg_apply, coe_neg, nnrealPart_sub_nnrealPart_neg, nnrealPart_neg_eq_zero_of_nonneg, exists_add_nnrealPart_add_eq
instNonUnitalCommRingOfIsTopologicalRing 📖	CompOp	—
instNonUnitalCommSemiringOfIsTopologicalSemiring 📖	CompOp	—
instNonUnitalNonAssocRingOfIsTopologicalRing 📖	CompOp	—
instNonUnitalNonAssocSemiringOfIsTopologicalSemiring 📖	CompOp	—
instNonUnitalRingOfIsTopologicalRing 📖	CompOp	—
instNonUnitalSemiringOfIsTopologicalSemiring 📖	CompOp	—
instSMulOfContinuousConstSMul 📖	CompOp	9 math math: nnrealPart_smul_neg, instStarModule, smul_apply, instSMulCommClass, coe_smul, instIsCentralScalar, toReal_smul, nnrealPart_smul_pos, instIsScalarTower
instSMulOfContinuousSMulOfContinuousMapClass 📖	CompOp	4 math math: instSMulCommClass, smulc_apply, coe_smulc, instIsScalarTower
instSMulWithZeroOfContinuousConstSMul 📖	CompOp	—
instSemigroupWithZeroOfContinuousMul 📖	CompOp	—
instStar 📖	CompOp	4 math math: star_apply, instStarModule, coe_star, instTrivialStar
instStarAddMonoid 📖	CompOp	—
instStarRing 📖	CompOp	—
instSub 📖	CompOp	3 math math: coe_sub, sub_apply, nnrealPart_sub_nnrealPart_neg
instSup 📖	CompOp	2 math math: sup_apply, coe_sup
instZero 📖	CompOp	6 math math: zero_comp, nnrealPart_neg_toReal_eq, coe_zero, zero_apply, toReal_nonneg, nnrealPart_neg_eq_zero_of_nonneg
nnrealPart 📖	CompOp	10 math math: nnrealPart_smul_neg, nnrealPart_add_le_add_nnrealPart, nnrealPart_neg_toReal_eq, toRealPositiveLinear_apply, nnrealPart_apply, nnrealPart_smul_pos, nnrealPart_toReal_eq, nnrealPart_sub_nnrealPart_neg, nnrealPart_neg_eq_zero_of_nonneg, exists_add_nnrealPart_add_eq
partialOrder 📖	CompOp	19 math math: instAddRightMono, nnrealPart_add_le_add_nnrealPart, RealRMK.rieszMeasure_le_of_eq_one, RealRMK.integral_rieszMeasure, toRealPositiveLinear_apply, le_def, instIsOrderedAddMonoid, toNNRealLinear_apply, TopologicalGroup.IsSES.pushforward_mono, lt_def, TopologicalAddGroup.IsSES.pushforward_mono, eq_toRealPositiveLinear_toReal, toReal_nonneg, integralPositiveLinearMap_toFun, instAddLeftMono, monotone_of_nnreal, instMulRightMono, RealRMK.le_rieszMeasure_tsupport_subset, instMulLeftMono
pullback_addMonoidHom 📖	CompOp	1 math math: pullback_addMonoidHom_def
pullback_monoidHom 📖	CompOp	1 math math: pullback_monoidHom_def
semilatticeInf 📖	CompOp	2 math math: finsetInf'_apply, coe_finsetInf'
semilatticeSup 📖	CompOp	2 math math: coe_finsetSup', finsetSup'_apply
toBoundedContinuousFunction 📖	CompOp	1 math math: toBoundedContinuousFunction_apply
toContinuousMap 📖	CompOp	3 math math: toContinuousMap_compLeft, coe_toContinuousMap, hasCompactSupport'
toNNRealLinear 📖	CompOp	3 math math: toNNRealLinear_inj, toNNRealLinear_apply, eq_toNNRealLinear_toRealPositiveLinear
toReal 📖	CompOp	12 math math: coe_toRealLinearMap, toRealLinearMap_apply, nnrealPart_neg_toReal_eq, toReal_apply, integralLinearMap_apply, toReal_add, toNNRealLinear_apply, toReal_smul, eq_toRealPositiveLinear_toReal, toReal_nonneg, nnrealPart_toReal_eq, nnrealPart_sub_nnrealPart_neg
toRealLinearMap 📖	CompOp	3 math math: toRealLinearMap_apply_apply, coe_toRealLinearMap, toRealLinearMap_apply
toRealPositiveLinear 📖	CompOp	3 math math: toRealPositiveLinear_apply, eq_toRealPositiveLinear_toReal, eq_toNNRealLinear_toRealPositiveLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero instFunLike instAddOfContinuousAdd AddZero.toAdd	—	—
coe_add 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero instFunLike instAddOfContinuousAdd Pi.instAdd AddZero.toAdd	—	—
coe_compLeft 📖	mathematical	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	DFunLike.coe CompactlySupportedContinuousMap instFunLike compLeft ContinuousMap ContinuousMap.instFunLike	—	—
coe_comp_to_continuous_fun 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike comp CocompactMap CocompactMap.instFunLike	—	—
coe_copy 📖	mathematical	DFunLike.coe CompactlySupportedContinuousMap instFunLike	DFunLike.coe CompactlySupportedContinuousMap instFunLike copy	—	—
coe_finsetInf' 📖	mathematical	Finset.Nonempty	DFunLike.coe CompactlySupportedContinuousMap instFunLike Finset.inf' semilatticeInf Pi.instSemilatticeInf	—	finsetInf'_apply Finset.inf'_apply
coe_finsetSup' 📖	mathematical	Finset.Nonempty	DFunLike.coe CompactlySupportedContinuousMap instFunLike Finset.sup' semilatticeSup Pi.instSemilatticeSup	—	finsetSup'_apply Finset.sup'_apply
coe_inf 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instInf Pi.instMinForall_mathlib SemilatticeInf.toMin	—	—
coe_mk 📖	mathematical	HasCompactSupport DFunLike.coe ContinuousMap ContinuousMap.instFunLike	DFunLike.coe CompactlySupportedContinuousMap instFunLike ContinuousMap ContinuousMap.instFunLike	—	—
coe_mul 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap MulZeroClass.toZero instFunLike instMulOfContinuousMul Pi.instMul MulZeroClass.toMul	—	—
coe_neg 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instNeg Pi.instNeg NegZeroClass.toNeg	—	—
coe_smul 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instSMulOfContinuousConstSMul Function.hasSMul SMulZeroClass.toSMul	—	—
coe_smulc 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instSMulOfContinuousSMulOfContinuousMapClass SMulZeroClass.toSMul	—	—
coe_star 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike Star.star instStar Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar	—	—
coe_sub 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
coe_sum 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike Finset.sum instAddCommMonoidOfContinuousAdd Pi.addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
coe_sup 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instSup Pi.instMaxForall_mathlib SemilatticeSup.toMax	—	—
coe_toContinuousMap 📖	mathematical	—	DFunLike.coe ContinuousMap ContinuousMap.instFunLike toContinuousMap CompactlySupportedContinuousMap instFunLike	—	—
coe_toRealLinearMap 📖	mathematical	—	DFunLike.coe LinearMap NNReal NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap NNReal.instZero NNReal.instTopologicalSpace Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instModuleOfContinuousConstSMul Semiring.toModule SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring NNReal.instModuleOfReal Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField LinearMap.instFunLike toRealLinearMap toReal	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul
coe_zero 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instZero Pi.instZero	—	—
compLeft_apply 📖	mathematical	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	DFunLike.coe CompactlySupportedContinuousMap instFunLike compLeft ContinuousMap ContinuousMap.instFunLike	—	coe_compLeft
comp_assoc 📖	mathematical	—	comp CocompactMap.comp	—	—
comp_id 📖	mathematical	—	comp CocompactMap.id	—	ext
continuousMapEquiv_apply_toFun 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike Equiv ContinuousMap EquivLike.toFunLike Equiv.instEquivLike continuousMapEquiv ContinuousMap.instFunLike	—	—
continuousMapEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv CompactlySupportedContinuousMap ContinuousMap EquivLike.toFunLike Equiv.instEquivLike Equiv.symm continuousMapEquiv toContinuousMap instFunLike	—	—
copy_eq 📖	mathematical	DFunLike.coe CompactlySupportedContinuousMap instFunLike	copy	—	DFunLike.ext'
eq_of_empty 📖	—	—	—	—	ext
eq_toNNRealLinear_toRealPositiveLinear 📖	mathematical	—	toNNRealLinear toRealPositiveLinear	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.ext NNReal.eq eq_toRealPositiveLinear_toReal
eq_toRealPositiveLinear_toReal 📖	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 toRealPositiveLinear toReal NNReal.toReal LinearMap NNReal NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring NNReal.instZero NNReal.instTopologicalSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap.instFunLike	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instIsTopologicalAddGroupReal nnrealPart_toReal_eq nnrealPart_neg_toReal_eq map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass sub_zero
exists_add_nnrealPart_add_eq 📖	mathematical	—	CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring IsSemitopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring nnrealPart Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instNeg Real.instAddGroup instIsTopologicalAddGroupReal	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instIsTopologicalAddGroupReal exists_add_of_le nnrealPart_add_le_add_nnrealPart ext NNReal.eq max_neg_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.LinearCombination.eq_of_eq instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
exists_add_of_le 📖	mathematical	CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder partialOrder NNReal.instPartialOrder	CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring IsSemitopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring NNReal.instContinuousSub IsCompact.of_isClosed_subset IsCompact.union hasCompactSupport' isClosed_closure tsupport.eq_1 closure_union closure_mono Mathlib.Tactic.Contrapose.contrapose₁ tsub_self ext NNReal.eq add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE NNReal.addLeftMono
ext 📖	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike	—	ext
finsetInf'_apply 📖	mathematical	Finset.Nonempty	DFunLike.coe CompactlySupportedContinuousMap instFunLike Finset.inf' semilatticeInf	—	Finset.comp_inf'_eq_inf'_comp
finsetSup'_apply 📖	mathematical	Finset.Nonempty	DFunLike.coe CompactlySupportedContinuousMap instFunLike Finset.sup' semilatticeSup	—	Finset.comp_sup'_eq_sup'_comp
hasCompactSupport 📖	mathematical	—	HasCompactSupport DFunLike.coe CompactlySupportedContinuousMap instFunLike	—	hasCompactSupport'
hasCompactSupport' 📖	mathematical	—	HasCompactSupport ContinuousMap.toFun toContinuousMap	—	—
inf_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instInf SemilatticeInf.toMin	—	—
instAddLeftMono 📖	mathematical	—	AddLeftMono CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero instAddOfContinuousAdd Preorder.toLE PartialOrder.toPreorder partialOrder	—	add_le_add_right
instAddRightMono 📖	mathematical	—	AddRightMono CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero instAddOfContinuousAdd Preorder.toLE PartialOrder.toPreorder partialOrder	—	add_le_add_left
instCompactlySupportedContinuousMapClass 📖	mathematical	—	CompactlySupportedContinuousMapClass CompactlySupportedContinuousMap instFunLike	—	ContinuousMap.continuous_toFun hasCompactSupport'
instIsCentralScalar 📖	mathematical	—	IsCentralScalar CompactlySupportedContinuousMap instSMulOfContinuousConstSMul SMulWithZero.toSMulZeroClass MulOpposite MulOpposite.instZero ContinuousConstSMul.op SMulZeroClass.toSMul	—	ContinuousConstSMul.op ext IsCentralScalar.op_smul_eq_smul
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidOfContinuousAdd PartialOrder.toPreorder partialOrder	—	add_le_add_left instAddRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono
instIsScalarTower 📖	mathematical	—	IsScalarTower CompactlySupportedContinuousMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instSMulOfContinuousConstSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSMulOfContinuousSMulOfContinuousMapClass NonUnitalNonAssocSemiring.toDistribSMul ContinuousMul.to_continuousSMul MulZeroClass.toMul IsTopologicalSemiring.toContinuousMul instFunLike CompactlySupportedContinuousMapClass.toContinuousMapClass instCompactlySupportedContinuousMapClass	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul CompactlySupportedContinuousMapClass.toContinuousMapClass instCompactlySupportedContinuousMapClass ext smul_eq_mul smul_assoc
instMulLeftMono 📖	mathematical	—	MulLeftMono CompactlySupportedContinuousMap MulZeroClass.toZero instMulOfContinuousMul Preorder.toLE PartialOrder.toPreorder partialOrder	—	mul_le_mul_right
instMulRightMono 📖	mathematical	—	MulRightMono CompactlySupportedContinuousMap MulZeroClass.toZero instMulOfContinuousMul Preorder.toLE PartialOrder.toPreorder partialOrder	—	mul_le_mul_left
instSMulCommClass 📖	mathematical	—	SMulCommClass CompactlySupportedContinuousMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass instSMulOfContinuousConstSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSMulOfContinuousSMulOfContinuousMapClass NonUnitalNonAssocSemiring.toDistribSMul ContinuousMul.to_continuousSMul MulZeroClass.toMul IsTopologicalSemiring.toContinuousMul instFunLike CompactlySupportedContinuousMapClass.toContinuousMapClass instCompactlySupportedContinuousMapClass	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul CompactlySupportedContinuousMapClass.toContinuousMapClass instCompactlySupportedContinuousMapClass ext smul_eq_mul SMulCommClass.smul_comm
instStarModule 📖	mathematical	—	StarModule CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instStar instSMulOfContinuousConstSMul SMulWithZero.toSMulZeroClass	—	ext StarModule.star_smul
instTrivialStar 📖	mathematical	—	TrivialStar CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instStar	—	ext TrivialStar.star_trivial
le_def 📖	mathematical	—	CompactlySupportedContinuousMap Preorder.toLE PartialOrder.toPreorder partialOrder DFunLike.coe instFunLike	—	Pi.le_def
lt_def 📖	mathematical	—	CompactlySupportedContinuousMap Preorder.toLT PartialOrder.toPreorder partialOrder Preorder.toLE DFunLike.coe instFunLike	—	Pi.lt_def
mul_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap MulZeroClass.toZero instFunLike instMulOfContinuousMul MulZeroClass.toMul	—	—
neg_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instNeg NegZeroClass.toNeg	—	—
nnrealPart_add_le_add_nnrealPart 📖	mathematical	—	CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder partialOrder NNReal.instPartialOrder nnrealPart Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass Real.instAddMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real.toNNReal_add_le
nnrealPart_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace instFunLike nnrealPart Real.toNNReal Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	—
nnrealPart_neg_eq_zero_of_nonneg 📖	mathematical	CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder partialOrder Real.partialOrder instZero	nnrealPart CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNeg Real.instAddGroup instIsTopologicalAddGroupReal NNReal NNReal.instZero NNReal.instTopologicalSpace instZero	—	ext instIsTopologicalAddGroupReal NNReal.eq IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
nnrealPart_neg_toReal_eq 📖	mathematical	—	nnrealPart CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instNeg Real.instAddGroup instIsTopologicalAddGroupReal toReal NNReal NNReal.instZero NNReal.instTopologicalSpace instZero	—	ext instIsTopologicalAddGroupReal NNReal.eq toReal_apply sup_of_le_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
nnrealPart_smul_neg 📖	mathematical	Real Real.instLE Real.instZero	nnrealPart Real CompactlySupportedContinuousMap Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSMulOfContinuousConstSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal NNReal NNReal.instZero NNReal.instTopologicalSpace AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real.toNNReal Real.instNeg instNeg Real.instAddGroup instIsTopologicalAddGroupReal	—	ext SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring instIsTopologicalAddGroupReal NNReal.eq le_total sup_of_le_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toPosMulStrictMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid sup_of_le_left MulZeroClass.mul_zero AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono Real.instIsOrderedRing covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add mul_neg neg_mul neg_neg
nnrealPart_smul_pos 📖	mathematical	Real Real.instLE Real.instZero	nnrealPart Real CompactlySupportedContinuousMap Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSMulOfContinuousConstSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass Real.instAddMonoid NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal NNReal NNReal.instZero NNReal.instTopologicalSpace AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real.toNNReal	—	ext SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring NNReal.eq sup_of_le_left le_total IsOrderedRing.toPosMulMono Real.instIsOrderedRing sup_of_le_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toPosMulStrictMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid MulZeroClass.mul_zero
nnrealPart_sub_nnrealPart_neg 📖	mathematical	—	CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instSub Real.instAddGroup instIsTopologicalAddGroupReal toReal nnrealPart instNeg	—	ext instIsTopologicalAddGroupReal toReal_apply max_zero_sub_max_neg_zero_eq_self IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
nnrealPart_toReal_eq 📖	mathematical	—	nnrealPart toReal	—	ext NNReal.eq toReal_apply Real.toNNReal_coe
pullback_addMonoidHom_def 📖	mathematical	Topology.IsClosedEmbedding DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom.instFunLike	DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instFunLike pullback_addMonoidHom AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddMonoidHom AddMonoidHom.instFunLike	—	—
pullback_monoidHom_def 📖	mathematical	Topology.IsClosedEmbedding DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike	DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instFunLike pullback_monoidHom MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom MonoidHom.instFunLike	—	—
smul_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instSMulOfContinuousConstSMul SMulZeroClass.toSMul	—	—
smulc_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instSMulOfContinuousSMulOfContinuousMapClass SMulZeroClass.toSMul	—	—
star_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike Star.star instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar	—	—
sub_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instFunLike instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	—
sum_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike Finset.sum instAddCommMonoidOfContinuousAdd	—	coe_sum Finset.sum_apply
sup_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instSup SemilatticeSup.toMax	—	—
toBoundedContinuousFunction_apply 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction BoundedContinuousFunction.instFunLike toBoundedContinuousFunction CompactlySupportedContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instFunLike	—	—
toContinuousMap_compLeft 📖	mathematical	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	toContinuousMap compLeft ContinuousMap.comp toContinuousMap CompactlySupportedContinuousMap instFunLike CompactlySupportedContinuousMapClass.toContinuousMapClass instCompactlySupportedContinuousMapClass	—	—
toNNRealLinear_apply 📖	mathematical	—	NNReal.toReal 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 MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring LinearMap.instFunLike toNNRealLinear PositiveLinearMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.semiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal partialOrder Real.partialOrder NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Real.instMul PositiveLinearMap.instFunLike toReal	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring
toNNRealLinear_inj 📖	mathematical	—	toNNRealLinear	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring PositiveLinearMap.ext instIsTopologicalAddGroupReal nnrealPart_sub_nnrealPart_neg map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass PositiveLinearMap.instLinearMapClass
toRealLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap NNReal NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap NNReal.instZero NNReal.instTopologicalSpace Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instModuleOfContinuousConstSMul Semiring.toModule SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring NNReal.instModuleOfReal Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField LinearMap.instFunLike toRealLinearMap toReal	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul
toRealLinearMap_apply_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instFunLike LinearMap NNReal NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring NNReal.instZero NNReal.instTopologicalSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal instModuleOfContinuousConstSMul Semiring.toModule SeparatelyContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring NNReal.instModuleOfReal Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField LinearMap.instFunLike toRealLinearMap NNReal.toReal	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul toReal_apply
toRealPositiveLinear_apply 📖	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 toRealPositiveLinear Real.instSub NNReal.toReal LinearMap NNReal NNReal.instSemiring RingHom.id Semiring.toNonAssocSemiring NNReal.instZero NNReal.instTopologicalSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap.instFunLike nnrealPart instNeg Real.instAddGroup instIsTopologicalAddGroupReal	—	IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal
toReal_add 📖	mathematical	—	toReal CompactlySupportedContinuousMap NNReal NNReal.instZero NNReal.instTopologicalSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring IsSemitopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal	—	ext IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal toReal_apply
toReal_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instFunLike toReal NNReal.toReal NNReal NNReal.instZero NNReal.instTopologicalSpace	—	compLeft_apply
toReal_nonneg 📖	mathematical	—	CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Preorder.toLE PartialOrder.toPreorder partialOrder Real.partialOrder instZero toReal	—	toReal_apply
toReal_smul 📖	mathematical	—	toReal NNReal CompactlySupportedContinuousMap NNReal.instZero NNReal.instTopologicalSpace instSMulOfContinuousConstSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring NNReal.instSemiring NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace SMulCommClass.continuousConstSMul Real.instMonoid SMulZeroClass.toSMul Algebra.to_smulCommClass NNReal.instCommSemiring NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsSemitopologicalRing.toIsSemitopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal	—	ext SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal toReal_apply
zero_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instZero	—	—
zero_comp 📖	mathematical	—	comp CompactlySupportedContinuousMap instZero	—	—

CompactlySupportedContinuousMap.ContinuousMap

Definitions

Name	Category	Theorems
liftCompactlySupported 📖	CompOp	—

CompactlySupportedContinuousMapClass

Definitions

Name	Category	Theorems
instCoeTCCompactlySupportedContinuousMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCompactSupport 📖	mathematical	—	HasCompactSupport DFunLike.coe	—	—
instZeroAtInftyContinuousMapClass 📖	mathematical	—	ZeroAtInftyContinuousMapClass	—	toContinuousMapClass HasCompactSupport.is_zero_at_infty hasCompactSupport
of_compactSpace 📖	mathematical	—	CompactlySupportedContinuousMapClass	—	HasCompactSupport.of_compactSpace
toContinuousMapClass 📖	mathematical	—	ContinuousMapClass	—	—
uniformContinuous 📖	mathematical	—	UniformContinuous DFunLike.coe	—	Continuous.uniformContinuous_of_tendsto_cocompact ContinuousMapClass.map_continuous toContinuousMapClass HasCompactSupport.is_zero_at_infty hasCompactSupport

(root)

Definitions

Name	Category	Theorems
CompactlySupportedContinuousMap 📖	CompData	106 math math: CompactlySupportedContinuousMap.coe_mk, CompactlySupportedContinuousMap.coe_sub, CompactlySupportedContinuousMap.coe_inf, CompactlySupportedContinuousMap.coe_mul, TopologicalGroup.IsSES.integral_inducedMeasure, CompactlySupportedContinuousMap.hasCompactSupport, CompactlySupportedContinuousMap.nnrealPart_smul_neg, CompactlySupportedContinuousMap.toBoundedContinuousFunction_apply, CompactlySupportedContinuousMap.zero_comp, TopologicalGroup.IsSES.integral_pullback_invFun_apply, TopologicalGroup.IsSES.pullback_def, TopologicalGroup.IsSES.pushforward_def, CompactlySupportedContinuousMap.star_apply, CompactlySupportedContinuousMap.instStarModule, CompactlySupportedContinuousMap.sub_apply, NNRealRMK.lintegral_rieszMeasure, CompactlySupportedContinuousMap.toRealLinearMap_apply_apply, CompactlySupportedContinuousMap.instAddRightMono, CompactlySupportedContinuousMap.coe_star, rieszContentAux_image_nonempty, CompactlySupportedContinuousMap.mul_apply, TopologicalAddGroup.IsSES.pushforward_apply_apply, CompactlySupportedContinuousMap.exists_add_of_le, CompactlySupportedContinuousMap.coe_toRealLinearMap, CompactlySupportedContinuousMap.smul_apply, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass, CompactlySupportedContinuousMap.instSMulCommClass, CompactlySupportedContinuousMap.coe_smul, RealRMK.rieszMeasure_le_of_eq_one, CompactlySupportedContinuousMap.toRealLinearMap_apply, RealRMK.integral_rieszMeasure, CompactlySupportedContinuousMap.integrable, CompactlySupportedContinuousMap.nnrealPart_neg_toReal_eq, CompactlySupportedContinuousMap.toContinuousMap_compLeft, CompactlySupportedContinuousMap.smulc_apply, CompactlySupportedContinuousMap.toRealPositiveLinear_apply, CompactlySupportedContinuousMap.sup_apply, CompactlySupportedContinuousMap.toReal_apply, CompactlySupportedContinuousMap.pullback_addMonoidHom_def, CompactlySupportedContinuousMap.compLeft_apply, CompactlySupportedContinuousMap.integralLinearMap_apply, TopologicalGroup.IsSES.integrate_apply, TopologicalAddGroup.IsSES.integrate_mono, CompactlySupportedContinuousMap.le_def, CompactlySupportedContinuousMap.ext_iff, CompactlySupportedContinuousMap.instIsCentralScalar, CompactlySupportedContinuousMap.coe_compLeft, CompactlySupportedContinuousMap.coe_copy, TopologicalGroup.IsSES.pushforward_apply_apply, CompactlySupportedContinuousMap.instIsOrderedAddMonoid, CompactlySupportedContinuousMap.instTrivialStar, TopologicalAddGroup.IsSES.integral_pullback_invFun_apply, CompactlySupportedContinuousMap.finsetInf'_apply, CompactlySupportedContinuousMap.inf_apply, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, CompactlySupportedContinuousMap.add_apply, CompactlySupportedContinuousMap.toReal_add, CompactlySupportedContinuousMap.coe_zero, CompactlySupportedContinuousMap.coe_sup, CompactlySupportedContinuousMap.zero_apply, CompactlySupportedContinuousMap.toNNRealLinear_apply, TopologicalAddGroup.IsSES.pushforward_def, CompactlySupportedContinuousMap.coe_toContinuousMap, CompactlySupportedContinuousMap.coe_smulc, NNRealRMK.le_rieszMeasure_of_tsupport_subset, CompactlySupportedContinuousMap.sum_apply, RealRMK.exists_open_approx, exists_lt_rieszContentAux_add_pos, TopologicalGroup.IsSES.pushforward_mono, CompactlySupportedContinuousMap.coe_comp_to_continuous_fun, CompactlySupportedContinuousMap.continuousMapEquiv_symm_apply, CompactlySupportedContinuousMap.toReal_smul, CompactlySupportedContinuousMap.lt_def, TopologicalAddGroup.IsSES.integral_inducedMeasure, CompactlySupportedContinuousMap.coe_finsetInf', CompactlySupportedContinuousMap.neg_apply, TopologicalAddGroup.IsSES.pushforward_mono, CompactlySupportedContinuousMap.nnrealPart_apply, CompactlySupportedContinuousMap.eq_toRealPositiveLinear_toReal, CompactlySupportedContinuousMap.toReal_nonneg, CompactlySupportedContinuousMap.nnrealPart_smul_pos, CompactlySupportedContinuousMap.integralPositiveLinearMap_toFun, CompactlySupportedContinuousMap.coe_neg, CompactlySupportedContinuousMap.coe_add, CompactlySupportedContinuousMap.instAddLeftMono, TopologicalAddGroup.IsSES.pullback_def, CompactlySupportedContinuousMap.coe_finsetSup', RealRMK.range_cut_partition, NNRealRMK.integral_rieszMeasure, CompactlySupportedContinuousMap.monotone_of_nnreal, CompactlySupportedContinuousMap.instMulRightMono, RealRMK.le_rieszMeasure_tsupport_subset, CompactlySupportedContinuousMap.instMulLeftMono, TopologicalGroup.IsSES.integrate_mono, exists_continuous_add_one_of_isCompact_nnreal, CompactlySupportedContinuousMap.pullback_monoidHom_def, CompactlySupportedContinuousMap.nnrealPart_sub_nnrealPart_neg, CompactlySupportedContinuousMap.instIsScalarTower, CompactlySupportedContinuousMap.finsetSup'_apply, CompactlySupportedContinuousMap.nnrealPart_neg_eq_zero_of_nonneg, CompactlySupportedContinuousMap.coe_sum, TopologicalAddGroup.IsSES.integrate_apply, CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq, rieszContentAux_le, CompactlySupportedContinuousMap.continuousMapEquiv_apply_toFun
CompactlySupportedContinuousMapClass 📖	CompData	2 math math: CompactlySupportedContinuousMapClass.of_compactSpace, CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass

---

← Back to Index