TestFunction

📁 Source: Mathlib/Analysis/Distribution/TestFunction.lean

Statistics

Metric	Count
Definitions «term𝓓(_,_)»»), «term𝓓^{_}(_,_)»»), TestFunction, coeFnAddMonoidHom, copy, instAdd, instAddCommGroup, instModuleOfSMulCommClassRealOfContinuousConstSMul, instNeg, instSMulOfSMulCommClassRealOfContinuousConstSMul, instSub, instZero, mkCLM, ofSupportedIn, ofSupportedInCLM, ofSupportedInLM, originalTop, postcompCLM, toBoundedContinuousFunctionCLM, toFun, toTestFunctionClass, topologicalSpace, uniformSpace, TestFunctionClass, toDFunLike	25
Theorems coeFnAddMonoidHom_apply, coe_add, coe_copy, coe_mk, coe_neg, coe_ofSupportedIn, coe_ofSupportedInCLM, coe_ofSupportedInLM, coe_smul, coe_sub, coe_toBoundedContinuousFunction, coe_zero, contDiff, contDiff', continuous_iff_continuous_comp, continuous_ofSupportedIn, copy_eq, ext, ext_iff, hasCompactSupport, hasCompactSupport', injective_toBoundedContinuousFunctionCLM, instContinuousSMulReal, instIsScalarTower, instIsTopologicalAddGroup, instIsUniformAddGroup, instLocallyConvexSpaceReal, instT3Space, mkCLM_apply, originalTop_le, postcompCLM_apply, toBoundedContinuousFunctionCLM_apply, toBoundedContinuousFunctionCLM_eq_of_scalars, toFun_eq_coe, topologicalSpace_le_iff, tsupport_subset, tsupport_subset', instBoundedContinuousMapClass, instContinuousMapClass, map_contDiff, map_hasCompactSupport, tsupport_map_subset	42
Total	67

Distributions

Definitions

Name	Category	Theorems
«term𝓓(_,_)» 📖» "API Documentation")	CompOp	—
«term𝓓^{_}(_,_)»(_,_)»} 📖» "API Documentation")	CompOp	—

TestFunction

Definitions

Name	Category	Theorems
coeFnAddMonoidHom 📖	CompOp	1 math math: coeFnAddMonoidHom_apply
copy 📖	CompOp	2 math math: copy_eq, coe_copy
instAdd 📖	CompOp	1 math math: coe_add
instAddCommGroup 📖	CompOp	13 math math: toBoundedContinuousFunctionCLM_eq_of_scalars, continuous_iff_continuous_comp, toBoundedContinuousFunctionCLM_apply, instIsUniformAddGroup, instIsTopologicalAddGroup, postcompCLM_apply, coe_ofSupportedInCLM, coe_ofSupportedInLM, Distribution.mapCLM_apply, mkCLM_apply, instLocallyConvexSpaceReal, coeFnAddMonoidHom_apply, injective_toBoundedContinuousFunctionCLM
instModuleOfSMulCommClassRealOfContinuousConstSMul 📖	CompOp	10 math math: toBoundedContinuousFunctionCLM_eq_of_scalars, continuous_iff_continuous_comp, toBoundedContinuousFunctionCLM_apply, postcompCLM_apply, coe_ofSupportedInCLM, coe_ofSupportedInLM, Distribution.mapCLM_apply, mkCLM_apply, instLocallyConvexSpaceReal, injective_toBoundedContinuousFunctionCLM
instNeg 📖	CompOp	1 math math: coe_neg
instSMulOfSMulCommClassRealOfContinuousConstSMul 📖	CompOp	3 math math: instIsScalarTower, coe_smul, instContinuousSMulReal
instSub 📖	CompOp	1 math math: coe_sub
instZero 📖	CompOp	1 math math: coe_zero
mkCLM 📖	CompOp	1 math math: mkCLM_apply
ofSupportedIn 📖	CompOp	5 math math: continuous_iff_continuous_comp, continuous_ofSupportedIn, coe_ofSupportedInCLM, coe_ofSupportedInLM, coe_ofSupportedIn
ofSupportedInCLM 📖	CompOp	2 math math: coe_ofSupportedInCLM, coe_ofSupportedInLM
ofSupportedInLM 📖	CompOp	—
originalTop 📖	CompOp	2 math math: topologicalSpace_le_iff, originalTop_le
postcompCLM 📖	CompOp	1 math math: postcompCLM_apply
toBoundedContinuousFunctionCLM 📖	CompOp	3 math math: toBoundedContinuousFunctionCLM_eq_of_scalars, toBoundedContinuousFunctionCLM_apply, injective_toBoundedContinuousFunctionCLM
toFun 📖	CompOp	4 math math: hasCompactSupport', contDiff', toFun_eq_coe, tsupport_subset'
toTestFunctionClass 📖	CompOp	16 math math: ext_iff, coe_neg, toBoundedContinuousFunctionCLM_apply, contDiff, coe_smul, postcompCLM_apply, coe_add, coe_zero, tsupport_subset, coe_sub, coe_ofSupportedIn, toFun_eq_coe, hasCompactSupport, coe_toBoundedContinuousFunction, coeFnAddMonoidHom_apply, coe_mk
topologicalSpace 📖	CompOp	16 math math: toBoundedContinuousFunctionCLM_eq_of_scalars, continuous_iff_continuous_comp, toBoundedContinuousFunctionCLM_apply, continuous_ofSupportedIn, instIsTopologicalAddGroup, postcompCLM_apply, coe_ofSupportedInCLM, coe_ofSupportedInLM, Distribution.mapCLM_apply, mkCLM_apply, instLocallyConvexSpaceReal, instContinuousSMulReal, instT3Space, topologicalSpace_le_iff, injective_toBoundedContinuousFunctionCLM, originalTop_le
uniformSpace 📖	CompOp	1 math math: instIsUniformAddGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFnAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom TestFunction AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddMonoidHom.instFunLike coeFnAddMonoidHom TestFunctionClass.toDFunLike toTestFunctionClass	—	—
coe_add 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	—
coe_copy 📖	mathematical	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	copy	—	—
coe_mk 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Set Set.instHasSubset tsupport SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	—	—
coe_neg 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
coe_ofSupportedIn 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass ofSupportedIn ContDiffMapSupportedIn ContDiffMapSupportedInClass.toDFunLike ContDiffMapSupportedIn.toContDiffMapSupportedInClass	—	—
coe_ofSupportedInCLM 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContDiffMapSupportedIn ContDiffMapSupportedIn.topologicalSpace AddCommGroup.toAddCommMonoid ContDiffMapSupportedIn.instAddCommGroup TestFunction topologicalSpace instAddCommGroup ContDiffMapSupportedIn.instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul instModuleOfSMulCommClassRealOfContinuousConstSMul ContinuousLinearMap.funLike ofSupportedInCLM ofSupportedIn	—	UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
coe_ofSupportedInLM 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContDiffMapSupportedIn ContDiffMapSupportedIn.topologicalSpace AddCommGroup.toAddCommMonoid ContDiffMapSupportedIn.instAddCommGroup TestFunction topologicalSpace instAddCommGroup ContDiffMapSupportedIn.instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul instModuleOfSMulCommClassRealOfContinuousConstSMul ContinuousLinearMap.funLike ofSupportedInCLM ofSupportedIn	—	coe_ofSupportedInCLM
coe_smul 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass instSMulOfSMulCommClassRealOfContinuousConstSMul Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	—
coe_sub 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—
coe_toBoundedContinuousFunction 📖	mathematical	—	DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instFunLike TestFunction TestFunctionClass.toDFunLike toTestFunctionClass TestFunctionClass.instBoundedContinuousMapClass BoundedContinuousMapClass.map_bounded	—	TestFunctionClass.instBoundedContinuousMapClass BoundedContinuousMapClass.map_bounded
coe_zero 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	—
contDiff 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	—	TestFunctionClass.map_contDiff
contDiff' 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat toFun	—	—
continuous_iff_continuous_comp 📖	mathematical	—	Continuous TestFunction topologicalSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup IsScalarTower.to_smulCommClass Real Real.instCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.normedField UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul LinearMap.instFunLike ContDiffMapSupportedIn ContDiffMapSupportedIn.topologicalSpace ofSupportedIn	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self LinearMap.IsScalarTower.compatibleSMul instIsScalarTower continuous_iff_le_induced topologicalAddGroup_induced DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass continuousSMul_induced SemilinearMapClass.toMulActionSemiHomClass LocallyConvexSpace.induced
continuous_ofSupportedIn 📖	mathematical	Set Set.instHasSubset SetLike.coe TopologicalSpace.Compacts UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TopologicalSpace.Compacts.instSetLike TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	Continuous ContDiffMapSupportedIn TestFunction ContDiffMapSupportedIn.topologicalSpace topologicalSpace ofSupportedIn	—	continuous_iff_coinduced_le le_trans le_iSup₂_of_le le_rfl originalTop_le
copy_eq 📖	mathematical	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	—	ext
hasCompactSupport 📖	mathematical	—	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	—	TestFunctionClass.map_hasCompactSupport
hasCompactSupport' 📖	mathematical	—	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup toFun	—	—
injective_toBoundedContinuousFunctionCLM 📖	mathematical	—	TestFunction BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup BoundedContinuousFunction.instPseudoMetricSpace BoundedContinuousFunction.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instBoundedAddOfLipschitzAdd AddCommMonoid.toAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring Real.normedField UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul BoundedContinuousFunction.instModule ContinuousLinearMap.funLike toBoundedContinuousFunctionCLM	—	—
instContinuousSMulReal 📖	mathematical	—	ContinuousSMul Real TestFunction instSMulOfSMulCommClassRealOfContinuousConstSMul Real.semiring NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul topologicalSpace	—	continuousSMul_sInf smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
instIsScalarTower 📖	mathematical	—	IsScalarTower TestFunction instSMulOfSMulCommClassRealOfContinuousConstSMul	—	ext smul_assoc
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup TestFunction topologicalSpace AddCommGroup.toAddGroup instAddCommGroup	—	topologicalAddGroup_sInf
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup TestFunction uniformSpace AddCommGroup.toAddGroup instAddCommGroup	—	isUniformAddGroup_of_addCommGroup instIsTopologicalAddGroup
instLocallyConvexSpaceReal 📖	mathematical	—	LocallyConvexSpace Real TestFunction Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul topologicalSpace	—	LocallyConvexSpace.sInf smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
instT3Space 📖	mathematical	—	T3Space TestFunction topologicalSpace	—	T2Space.of_injective_continuous TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul injective_toBoundedContinuousFunctionCLM ContinuousLinearMap.continuous instT3Space T1Space.t0Space T2Space.t1Space IsTopologicalAddGroup.regularSpace instIsTopologicalAddGroup
mkCLM_apply 📖	mathematical	TestFunction instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instSMulOfSMulCommClassRealOfContinuousConstSMul DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup IsScalarTower.to_smulCommClass Real Real.instCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.normedField UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Continuous ContDiffMapSupportedIn ContDiffMapSupportedIn.topologicalSpace ofSupportedIn	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring topologicalSpace instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul ContinuousLinearMap.funLike mkCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
originalTop_le 📖	mathematical	—	TopologicalSpace TestFunction Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder originalTop topologicalSpace	—	le_sInf
postcompCLM_apply 📖	mathematical	—	DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup IsScalarTower.to_smulCommClass Real Real.instCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.normedField UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike postcompCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
toBoundedContinuousFunctionCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instPseudoMetricSpace BoundedContinuousFunction.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instBoundedAddOfLipschitzAdd AddCommMonoid.toAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring Real.normedField UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul BoundedContinuousFunction.instModule ContinuousLinearMap.funLike toBoundedContinuousFunctionCLM TestFunctionClass.toDFunLike toTestFunctionClass	—	instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
toBoundedContinuousFunctionCLM_eq_of_scalars 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup BoundedContinuousFunction.instPseudoMetricSpace BoundedContinuousFunction.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instBoundedAddOfLipschitzAdd AddCommMonoid.toAddMonoid SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup instModuleOfSMulCommClassRealOfContinuousConstSMul NormedSpace.toModule IsScalarTower.to_smulCommClass Real Real.instCommSemiring Real.normedField UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul BoundedContinuousFunction.instModule ContinuousLinearMap.funLike toBoundedContinuousFunctionCLM	—	instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass	—	—
topologicalSpace_le_iff 📖	mathematical	—	TopologicalSpace TestFunction Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder topologicalSpace originalTop	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul le_trans originalTop_le sInf_le
tsupport_subset 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe TestFunction TestFunctionClass.toDFunLike toTestFunctionClass SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	TestFunctionClass.tsupport_map_subset
tsupport_subset' 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	—

TestFunctionClass

Definitions

Name	Category	Theorems
toDFunLike 📖	CompOp	21 math math: instContinuousMapClass, TestFunction.ext_iff, TestFunction.coe_neg, TestFunction.toBoundedContinuousFunctionCLM_apply, TestFunction.contDiff, TestFunction.coe_smul, TestFunction.postcompCLM_apply, instBoundedContinuousMapClass, map_hasCompactSupport, TestFunction.coe_add, TestFunction.coe_zero, TestFunction.tsupport_subset, TestFunction.coe_sub, TestFunction.coe_ofSupportedIn, TestFunction.toFun_eq_coe, TestFunction.hasCompactSupport, TestFunction.coe_toBoundedContinuousFunction, tsupport_map_subset, TestFunction.coeFnAddMonoidHom_apply, map_contDiff, TestFunction.coe_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBoundedContinuousMapClass 📖	mathematical	—	BoundedContinuousMapClass UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toDFunLike	—	instContinuousMapClass Continuous.bounded_above_of_compact_support ContinuousMapClass.map_continuous map_hasCompactSupport BoundedContinuousMapClass.map_bounded BoundedContinuousFunction.instBoundedContinuousMapClass
instContinuousMapClass 📖	mathematical	—	ContinuousMapClass UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toDFunLike	—	ContDiff.continuous map_contDiff
map_contDiff 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField WithTop.some ENat DFunLike.coe toDFunLike	—	—
map_hasCompactSupport 📖	mathematical	—	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe toDFunLike	—	—
tsupport_map_subset 📖	mathematical	—	Set Set.instHasSubset tsupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe toDFunLike SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike	—	—

(root)

Definitions

Name	Category	Theorems
TestFunction 📖	CompData	31 math math: TestFunction.ext_iff, TestFunction.coe_neg, TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars, TestFunction.continuous_iff_continuous_comp, TestFunction.toBoundedContinuousFunctionCLM_apply, TestFunction.instIsUniformAddGroup, TestFunction.contDiff, TestFunction.continuous_ofSupportedIn, TestFunction.instIsScalarTower, TestFunction.instIsTopologicalAddGroup, TestFunction.coe_smul, TestFunction.postcompCLM_apply, TestFunction.coe_ofSupportedInCLM, TestFunction.coe_ofSupportedInLM, Distribution.mapCLM_apply, TestFunction.coe_add, TestFunction.coe_zero, TestFunction.tsupport_subset, TestFunction.coe_sub, TestFunction.coe_ofSupportedIn, TestFunction.toFun_eq_coe, TestFunction.instLocallyConvexSpaceReal, TestFunction.hasCompactSupport, TestFunction.coe_toBoundedContinuousFunction, TestFunction.instContinuousSMulReal, TestFunction.instT3Space, TestFunction.coeFnAddMonoidHom_apply, TestFunction.topologicalSpace_le_iff, TestFunction.injective_toBoundedContinuousFunctionCLM, TestFunction.coe_mk, TestFunction.originalTop_le
TestFunctionClass 📖	CompData	—

---

← Back to Index