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, semilatticeInf, semilatticeSup, toBoundedContinuousFunction, toContinuousMap, toNNRealLinear, toReal, toRealLinearMap, toRealPositiveLinear, CompactlySupportedContinuousMapClass, instCoeTCCompactlySupportedContinuousMap	56
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, 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	85
Total	141

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	22 math math: NNRealRMK.lintegral_rieszMeasure, toRealLinearMap_apply_apply, rieszContentAux_image_nonempty, coe_toRealLinearMap, RealRMK.rieszMeasure_le_of_eq_one, toRealLinearMap_apply, RealRMK.integral_rieszMeasure, toRealPositiveLinear_apply, integralLinearMap_apply, instIsOrderedAddMonoid, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, toNNRealLinear_apply, NNRealRMK.le_rieszMeasure_of_tsupport_subset, sum_apply, exists_lt_rieszContentAux_add_pos, eq_toRealPositiveLinear_toReal, integralPositiveLinearMap_toFun, NNRealRMK.integral_rieszMeasure, monotone_of_nnreal, RealRMK.le_rieszMeasure_tsupport_subset, coe_sum, 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	53 math math: coe_mk, coe_sub, coe_inf, coe_mul, hasCompactSupport, toBoundedContinuousFunction_apply, star_apply, sub_apply, NNRealRMK.lintegral_rieszMeasure, toRealLinearMap_apply_apply, coe_star, mul_apply, smul_apply, instCompactlySupportedContinuousMapClass, instSMulCommClass, coe_smul, RealRMK.integral_rieszMeasure, integrable, toContinuousMap_compLeft, smulc_apply, sup_apply, toReal_apply, compLeft_apply, integralLinearMap_apply, le_def, ext_iff, coe_compLeft, finsetInf'_apply, inf_apply, add_apply, coe_zero, coe_sup, zero_apply, coe_toContinuousMap, coe_smulc, sum_apply, exists_lt_rieszContentAux_add_pos, coe_comp_to_continuous_fun, continuousMapEquiv_symm_apply, lt_def, coe_finsetInf', neg_apply, nnrealPart_apply, integralPositiveLinearMap_toFun, coe_neg, coe_add, coe_finsetSup', NNRealRMK.integral_rieszMeasure, exists_continuous_add_one_of_isCompact_nnreal, instIsScalarTower, finsetSup'_apply, coe_sum, continuousMapEquiv_apply_toFun
instInf 📖	CompOp	2 math math: coe_inf, inf_apply
instInhabited 📖	CompOp	—
instLatticeOfTopologicalLattice 📖	CompOp	—
instModuleOfContinuousConstSMul 📖	CompOp	19 math math: NNRealRMK.lintegral_rieszMeasure, toRealLinearMap_apply_apply, rieszContentAux_image_nonempty, coe_toRealLinearMap, RealRMK.rieszMeasure_le_of_eq_one, toRealLinearMap_apply, RealRMK.integral_rieszMeasure, toRealPositiveLinear_apply, integralLinearMap_apply, NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subset, toNNRealLinear_apply, NNRealRMK.le_rieszMeasure_of_tsupport_subset, exists_lt_rieszContentAux_add_pos, eq_toRealPositiveLinear_toReal, integralPositiveLinearMap_toFun, NNRealRMK.integral_rieszMeasure, monotone_of_nnreal, RealRMK.le_rieszMeasure_tsupport_subset, 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	5 math math: zero_comp, nnrealPart_neg_toReal_eq, coe_zero, zero_apply, toReal_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	17 math math: instAddRightMono, nnrealPart_add_le_add_nnrealPart, RealRMK.rieszMeasure_le_of_eq_one, RealRMK.integral_rieszMeasure, toRealPositiveLinear_apply, le_def, instIsOrderedAddMonoid, toNNRealLinear_apply, lt_def, eq_toRealPositiveLinear_toReal, toReal_nonneg, integralPositiveLinearMap_toFun, instAddLeftMono, monotone_of_nnreal, instMulRightMono, RealRMK.le_rieszMeasure_tsupport_subset, instMulLeftMono
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	CompactlySupportedContinuousMap instFunLike compLeft	—	—
coe_comp_to_continuous_fun 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike comp CocompactMap CocompactMap.instFunLike	—	—
coe_copy 📖	mathematical	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	CompactlySupportedContinuousMap 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 instSemiringNNReal RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap instZeroNNReal NNReal.instTopologicalSpace Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instModuleOfContinuousConstSMul Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul 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 NNReal.instModuleOfReal Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instFunLike toRealLinearMap toReal	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul
coe_zero 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap instFunLike instZero Pi.instZero	—	—
compLeft_apply 📖	mathematical	DFunLike.coe ContinuousMap ContinuousMap.instFunLike	CompactlySupportedContinuousMap instFunLike compLeft	—	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	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul 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 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 toRealPositiveLinear toReal NNReal.toReal LinearMap NNReal instSemiringNNReal RingHom.id Semiring.toNonAssocSemiring instZeroNNReal NNReal.instTopologicalSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instIsTopologicalSemiring Semiring.toModule instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul LinearMap.instFunLike	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul 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 instZeroNNReal NNReal.instTopologicalSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring 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 IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instNeg Real.instAddGroup instIsTopologicalAddGroupReal	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 instZeroNNReal NNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder partialOrder instPartialOrderNNReal	instAddOfContinuousAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instIsTopologicalSemiring	—	IsTopologicalSemiring.toContinuousAdd 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 NNReal.instCanonicallyOrderedAdd NNReal.instOrderedSub 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	—	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 instZeroNNReal NNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder partialOrder instPartialOrderNNReal nnrealPart Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass Real.instAddMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instIsTopologicalSemiring	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NNReal.instIsTopologicalSemiring Real.toNNReal_add_le
nnrealPart_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap NNReal instZeroNNReal 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 instNeg Real.instAddGroup instIsTopologicalAddGroupReal NNReal instZeroNNReal NNReal.instTopologicalSpace	—	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 instZeroNNReal 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 CompactlySupportedContinuousMap 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 UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NNReal instZeroNNReal NNReal.instTopologicalSpace AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal NonAssocSemiring.toNonUnitalNonAssocSemiring instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul Real.toNNReal Real.instNeg instNeg Real.instAddGroup instIsTopologicalAddGroupReal	—	ext UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul instIsTopologicalAddGroupReal NNReal.eq le_total sup_of_le_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toPosMulStrictMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd 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 AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add mul_neg neg_mul neg_neg
nnrealPart_smul_pos 📖	mathematical	Real Real.instLE Real.instZero	nnrealPart CompactlySupportedContinuousMap 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 UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal NNReal instZeroNNReal NNReal.instTopologicalSpace AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal NonAssocSemiring.toNonUnitalNonAssocSemiring instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul Real.toNNReal	—	ext UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul 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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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
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 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 toNNRealLinear PositiveLinearMap Real Real.instZero UniformSpace.toTopologicalSpace Real.pseudoMetricSpace Real.semiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal partialOrder Real.partialOrder NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing PositiveLinearMap.instFunLike toReal	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul
toNNRealLinear_inj 📖	mathematical	—	toNNRealLinear	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul PositiveLinearMap.ext instIsTopologicalAddGroupReal nnrealPart_sub_nnrealPart_neg map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass PositiveLinearMap.instLinearMapClass
toRealLinearMap_apply 📖	mathematical	—	DFunLike.coe LinearMap NNReal instSemiringNNReal RingHom.id Semiring.toNonAssocSemiring CompactlySupportedContinuousMap instZeroNNReal NNReal.instTopologicalSpace Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instModuleOfContinuousConstSMul Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul 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 NNReal.instModuleOfReal Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instFunLike toRealLinearMap toReal	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul
toRealLinearMap_apply_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instFunLike LinearMap NNReal instSemiringNNReal RingHom.id Semiring.toNonAssocSemiring instZeroNNReal NNReal.instTopologicalSpace instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring Real.instAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instModuleOfContinuousConstSMul Semiring.toModule UniformContinuousConstSMul.to_continuousConstSMul 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 NNReal.instModuleOfReal Real.semiring NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.instFunLike toRealLinearMap NNReal.toReal	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul toReal_apply
toRealPositiveLinear_apply 📖	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 toRealPositiveLinear Real.instSub NNReal.toReal LinearMap NNReal instSemiringNNReal RingHom.id Semiring.toNonAssocSemiring instZeroNNReal NNReal.instTopologicalSpace NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instIsTopologicalSemiring Semiring.toModule instPseudoMetricSpaceNNReal IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul LinearMap.instFunLike nnrealPart instNeg Real.instAddGroup instIsTopologicalAddGroupReal	—	IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul
toReal_add 📖	mathematical	—	toReal CompactlySupportedContinuousMap NNReal instZeroNNReal NNReal.instTopologicalSpace instAddOfContinuousAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring 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 IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	—	ext IsTopologicalSemiring.toContinuousAdd NNReal.instIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal toReal_apply
toReal_apply 📖	mathematical	—	DFunLike.coe CompactlySupportedContinuousMap Real Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instFunLike toReal NNReal.toReal NNReal instZeroNNReal 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 instZeroNNReal NNReal.instTopologicalSpace instSMulOfContinuousConstSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instSemiringNNReal NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal SMulZeroClass.toSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul Real Real.instZero UniformSpace.toTopologicalSpace 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 Algebra.to_smulCommClass instCommSemiringNNReal NNReal.instAlgebraOfReal Algebra.id Real.instCommSemiring IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal	—	ext UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NNReal.isBoundedSMul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring 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	78 math math: CompactlySupportedContinuousMap.coe_mk, CompactlySupportedContinuousMap.coe_sub, CompactlySupportedContinuousMap.coe_inf, CompactlySupportedContinuousMap.coe_mul, CompactlySupportedContinuousMap.hasCompactSupport, CompactlySupportedContinuousMap.nnrealPart_smul_neg, CompactlySupportedContinuousMap.toBoundedContinuousFunction_apply, CompactlySupportedContinuousMap.zero_comp, 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, CompactlySupportedContinuousMap.coe_toRealLinearMap, CompactlySupportedContinuousMap.smul_apply, CompactlySupportedContinuousMap.nnrealPart_add_le_add_nnrealPart, CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass, CompactlySupportedContinuousMap.instSMulCommClass, CompactlySupportedContinuousMap.coe_smul, 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.compLeft_apply, CompactlySupportedContinuousMap.integralLinearMap_apply, CompactlySupportedContinuousMap.le_def, CompactlySupportedContinuousMap.ext_iff, CompactlySupportedContinuousMap.instIsCentralScalar, CompactlySupportedContinuousMap.coe_compLeft, CompactlySupportedContinuousMap.instIsOrderedAddMonoid, CompactlySupportedContinuousMap.instTrivialStar, CompactlySupportedContinuousMap.finsetInf'_apply, CompactlySupportedContinuousMap.inf_apply, CompactlySupportedContinuousMap.add_apply, CompactlySupportedContinuousMap.toReal_add, CompactlySupportedContinuousMap.coe_zero, CompactlySupportedContinuousMap.coe_sup, CompactlySupportedContinuousMap.zero_apply, CompactlySupportedContinuousMap.toNNRealLinear_apply, CompactlySupportedContinuousMap.coe_toContinuousMap, CompactlySupportedContinuousMap.coe_smulc, CompactlySupportedContinuousMap.sum_apply, exists_lt_rieszContentAux_add_pos, CompactlySupportedContinuousMap.coe_comp_to_continuous_fun, CompactlySupportedContinuousMap.continuousMapEquiv_symm_apply, CompactlySupportedContinuousMap.toReal_smul, CompactlySupportedContinuousMap.lt_def, CompactlySupportedContinuousMap.coe_finsetInf', CompactlySupportedContinuousMap.neg_apply, 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, CompactlySupportedContinuousMap.coe_finsetSup', NNRealRMK.integral_rieszMeasure, CompactlySupportedContinuousMap.monotone_of_nnreal, CompactlySupportedContinuousMap.instMulRightMono, CompactlySupportedContinuousMap.instMulLeftMono, exists_continuous_add_one_of_isCompact_nnreal, CompactlySupportedContinuousMap.nnrealPart_sub_nnrealPart_neg, CompactlySupportedContinuousMap.instIsScalarTower, CompactlySupportedContinuousMap.finsetSup'_apply, CompactlySupportedContinuousMap.coe_sum, CompactlySupportedContinuousMap.exists_add_nnrealPart_add_eq, CompactlySupportedContinuousMap.continuousMapEquiv_apply_toFun
CompactlySupportedContinuousMapClass 📖	CompData	2 math math: CompactlySupportedContinuousMapClass.of_compactSpace, CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass

---

← Back to Index