TestFunction

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

Statistics

Metric	Count
Definitions «term𝓓(_,_)»»), «term𝓓^{_}(_,_)»»), TestFunction, coeFnAddMonoidHom, copy, fderivCLM, instAdd, instAddCommGroup, instLineDerivTopENat, instModuleOfSMulCommClassRealOfContinuousConstSMul, instNeg, instSMulOfSMulCommClassRealOfContinuousConstSMul, instSub, instZero, limitCLM, lineDerivCLM, mkCLM, monoCLM, ofSupportedIn, ofSupportedInCLM, ofSupportedInLM, originalTop, postcompCLM, toBoundedContinuousFunctionCLM, toFun, toTestFunctionClass, topologicalSpace, uniformSpace, TestFunctionClass, toDFunLike	30
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, fderivCLM_apply, fderivCLM_apply_of_gt, fderivCLM_apply_of_le, fderivCLM_eq_of_scalars, fderivCLM_ofSupportedIn, hasCompactSupport, hasCompactSupport', injective_toBoundedContinuousFunctionCLM, instContinuousEval, instContinuousLineDerivTopENat, instContinuousSMulReal, instIsScalarTower, instIsTopologicalAddGroup, instIsUniformAddGroup, instLineDerivAddTopENat, instLineDerivLeftSMulRealTopENat, instLineDerivSMulTopENat, instLocallyConvexSpaceReal, instT3Space, limitCLM_apply, lineDerivCLM_add, lineDerivCLM_apply, lineDerivCLM_apply_of_gt, lineDerivCLM_apply_of_le, lineDerivCLM_eq_fderivCLM, lineDerivCLM_eq_of_scalars, lineDerivCLM_smul, lineDerivOpCLM_eq_lineDerivCLM, lineDerivOp_eq_lineDerivCLM, mkCLM_apply, monoCLM_apply, monoCLM_eq_of_scalars, monoCLM_eq_zero, 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	65
Total	95

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
fderivCLM 📖	CompOp	6 math math: fderivCLM_apply_of_le, fderivCLM_ofSupportedIn, lineDerivCLM_eq_fderivCLM, fderivCLM_eq_of_scalars, fderivCLM_apply_of_gt, fderivCLM_apply
instAdd 📖	CompOp	1 math math: coe_add
instAddCommGroup 📖	CompOp	34 math math: lineDerivCLM_apply_of_le, Distribution.delta_apply, toBoundedContinuousFunctionCLM_eq_of_scalars, monoCLM_eq_zero, continuous_iff_continuous_comp, toBoundedContinuousFunctionCLM_apply, instIsUniformAddGroup, fderivCLM_apply_of_le, lineDerivOpCLM_eq_lineDerivCLM, fderivCLM_ofSupportedIn, limitCLM_apply, instIsTopologicalAddGroup, postcompCLM_apply, Distribution.delta_eq_zero_of_notMem, coe_ofSupportedInCLM, instLineDerivAddTopENat, coe_ofSupportedInLM, lineDerivCLM_add, Distribution.mapCLM_apply, lineDerivOp_eq_lineDerivCLM, lineDerivCLM_eq_fderivCLM, lineDerivCLM_apply, monoCLM_eq_of_scalars, mkCLM_apply, fderivCLM_eq_of_scalars, lineDerivCLM_eq_of_scalars, fderivCLM_apply_of_gt, lineDerivCLM_smul, monoCLM_apply, instLocallyConvexSpaceReal, fderivCLM_apply, lineDerivCLM_apply_of_gt, coeFnAddMonoidHom_apply, injective_toBoundedContinuousFunctionCLM
instLineDerivTopENat 📖	CompOp	6 math math: lineDerivOpCLM_eq_lineDerivCLM, instContinuousLineDerivTopENat, instLineDerivAddTopENat, lineDerivOp_eq_lineDerivCLM, instLineDerivLeftSMulRealTopENat, instLineDerivSMulTopENat
instModuleOfSMulCommClassRealOfContinuousConstSMul 📖	CompOp	30 math math: lineDerivCLM_apply_of_le, Distribution.delta_apply, toBoundedContinuousFunctionCLM_eq_of_scalars, monoCLM_eq_zero, continuous_iff_continuous_comp, toBoundedContinuousFunctionCLM_apply, fderivCLM_apply_of_le, lineDerivOpCLM_eq_lineDerivCLM, fderivCLM_ofSupportedIn, limitCLM_apply, postcompCLM_apply, Distribution.delta_eq_zero_of_notMem, coe_ofSupportedInCLM, coe_ofSupportedInLM, lineDerivCLM_add, Distribution.mapCLM_apply, lineDerivOp_eq_lineDerivCLM, lineDerivCLM_eq_fderivCLM, lineDerivCLM_apply, monoCLM_eq_of_scalars, mkCLM_apply, fderivCLM_eq_of_scalars, lineDerivCLM_eq_of_scalars, fderivCLM_apply_of_gt, lineDerivCLM_smul, monoCLM_apply, instLocallyConvexSpaceReal, fderivCLM_apply, lineDerivCLM_apply_of_gt, injective_toBoundedContinuousFunctionCLM
instNeg 📖	CompOp	1 math math: coe_neg
instSMulOfSMulCommClassRealOfContinuousConstSMul 📖	CompOp	5 math math: instIsScalarTower, coe_smul, instLineDerivLeftSMulRealTopENat, instLineDerivSMulTopENat, instContinuousSMulReal
instSub 📖	CompOp	1 math math: coe_sub
instZero 📖	CompOp	2 math math: coe_zero, monoCLM_apply
limitCLM 📖	CompOp	1 math math: limitCLM_apply
lineDerivCLM 📖	CompOp	9 math math: lineDerivCLM_apply_of_le, lineDerivOpCLM_eq_lineDerivCLM, lineDerivCLM_add, lineDerivOp_eq_lineDerivCLM, lineDerivCLM_eq_fderivCLM, lineDerivCLM_apply, lineDerivCLM_eq_of_scalars, lineDerivCLM_smul, lineDerivCLM_apply_of_gt
mkCLM 📖	CompOp	1 math math: mkCLM_apply
monoCLM 📖	CompOp	3 math math: monoCLM_eq_zero, monoCLM_eq_of_scalars, monoCLM_apply
ofSupportedIn 📖	CompOp	6 math math: continuous_iff_continuous_comp, fderivCLM_ofSupportedIn, 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	25 math math: lineDerivCLM_apply_of_le, Distribution.delta_apply, ext_iff, coe_neg, toBoundedContinuousFunctionCLM_apply, fderivCLM_apply_of_le, contDiff, coe_smul, postcompCLM_apply, instContinuousEval, lineDerivCLM_eq_fderivCLM, lineDerivCLM_apply, coe_add, coe_zero, tsupport_subset, coe_sub, coe_ofSupportedIn, toFun_eq_coe, monoCLM_apply, coe_copy, hasCompactSupport, fderivCLM_apply, coe_toBoundedContinuousFunction, coeFnAddMonoidHom_apply, coe_mk
topologicalSpace 📖	CompOp	38 math math: lineDerivCLM_apply_of_le, Distribution.delta_apply, toBoundedContinuousFunctionCLM_eq_of_scalars, monoCLM_eq_zero, continuous_iff_continuous_comp, toBoundedContinuousFunctionCLM_apply, fderivCLM_apply_of_le, lineDerivOpCLM_eq_lineDerivCLM, fderivCLM_ofSupportedIn, continuous_ofSupportedIn, limitCLM_apply, instContinuousLineDerivTopENat, instIsTopologicalAddGroup, postcompCLM_apply, Distribution.delta_eq_zero_of_notMem, coe_ofSupportedInCLM, instContinuousEval, coe_ofSupportedInLM, lineDerivCLM_add, Distribution.mapCLM_apply, lineDerivOp_eq_lineDerivCLM, lineDerivCLM_eq_fderivCLM, lineDerivCLM_apply, monoCLM_eq_of_scalars, mkCLM_apply, fderivCLM_eq_of_scalars, lineDerivCLM_eq_of_scalars, fderivCLM_apply_of_gt, lineDerivCLM_smul, monoCLM_apply, instLocallyConvexSpaceReal, fderivCLM_apply, instContinuousSMulReal, lineDerivCLM_apply_of_gt, 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	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 NormedAddCommGroup.toSeminormedAddCommGroup UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace 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 NormedAddCommGroup.toSeminormedAddCommGroup UniformContinuousConstSMul.to_continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace 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
fderivCLM_apply 📖	mathematical	—	DFunLike.coe TestFunction ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing TestFunctionClass.toDFunLike toTestFunctionClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul IsScalarTower.to_smulCommClass Real.instCommSemiring 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 SeminormedRing.toPseudoMetricSpace 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.module SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike fderivCLM ENat instLEENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat LinearOrder.toDecidableLE instLinearOrderENat fderiv Pi.instZero ContinuousLinearMap.zero	—	RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup fderivCLM.eq_1 limitCLM.congr_simp
fderivCLM_apply_of_gt 📖	mathematical	ENat instLTENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	fderivCLM ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instModuleOfSMulCommClassRealOfContinuousConstSMul IsScalarTower.to_smulCommClass Real.instCommSemiring 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 SeminormedRing.toPseudoMetricSpace 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.module SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.zero	—	ContinuousLinearMap.ext RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ext fderivCLM_apply not_le_of_gt
fderivCLM_apply_of_le 📖	mathematical	ENat instLEENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	DFunLike.coe TestFunction ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing TestFunctionClass.toDFunLike toTestFunctionClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul IsScalarTower.to_smulCommClass Real.instCommSemiring 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 SeminormedRing.toPseudoMetricSpace 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.module SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike fderivCLM fderiv	—	RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup fderivCLM_apply
fderivCLM_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 Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instModuleOfSMulCommClassRealOfContinuousConstSMul IsScalarTower.to_smulCommClass Real.instCommSemiring 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 SeminormedRing.toPseudoMetricSpace 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.module SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike fderivCLM	—	RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup
fderivCLM_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 ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup Real Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Real.commRing instModuleOfSMulCommClassRealOfContinuousConstSMul IsScalarTower.to_smulCommClass Real.instCommSemiring 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 SeminormedRing.toPseudoMetricSpace 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.module SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.funLike fderivCLM ofSupportedIn ContDiffMapSupportedIn ContDiffMapSupportedIn.topologicalSpace ContDiffMapSupportedIn.instAddCommGroup ContDiffMapSupportedIn.instModuleOfSMulCommClassRealOfContinuousConstSMul ContDiffMapSupportedIn.fderivCLM	—	ext RingHomIsometric.ids smulCommClass_self IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.ext fderivCLM_apply ContDiffMapSupportedIn.fderivCLM_apply
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 ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid 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 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	—	—
instContinuousEval 📖	mathematical	—	ContinuousEval TestFunction TestFunctionClass.toDFunLike toTestFunctionClass topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	ContinuousEval.of_continuous_forget BoundedContinuousFunction.instContinuousEval instBoundedAddOfLipschitzAdd SeminormedAddCommGroup.to_lipschitzAdd IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.to_smulCommClass IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.continuous
instContinuousLineDerivTopENat 📖	mathematical	—	ContinuousLineDeriv TestFunction Top.top ENat instTopENat topologicalSpace instLineDerivTopENat	—	ContinuousLinearMap.continuous IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
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
instLineDerivAddTopENat 📖	mathematical	—	LineDerivAdd TestFunction Top.top ENat instTopENat NormedAddCommGroup.toAddCommGroup instAddCommGroup instLineDerivTopENat	—	map_add IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup lineDerivCLM_add
instLineDerivLeftSMulRealTopENat 📖	mathematical	—	LineDerivLeftSMul Real TestFunction Top.top ENat instTopENat 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField instSMulOfSMulCommClassRealOfContinuousConstSMul smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul instLineDerivTopENat	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass IsScalarTower.to_smulCommClass' instIsScalarTower ContinuousSMul.continuousConstSMul instContinuousSMulReal lineDerivCLM_smul
instLineDerivSMulTopENat 📖	mathematical	—	LineDerivSMul TestFunction Top.top ENat instTopENat 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 instLineDerivTopENat	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
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
limitCLM_apply 📖	mathematical	ofSupportedIn DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ContDiffMapSupportedIn ContDiffMapSupportedIn.topologicalSpace AddCommGroup.toAddCommMonoid ContDiffMapSupportedIn.instAddCommGroup ContDiffMapSupportedIn.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	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction 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 limitCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
lineDerivCLM_add 📖	mathematical	—	lineDerivCLM AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup 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 ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup instIsTopologicalAddGroup	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup ext RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup fderivCLM_apply map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
lineDerivCLM_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 lineDerivCLM ENat instLEENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat LinearOrder.toDecidableLE instLinearOrderENat lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup lineDerivCLM_eq_fderivCLM fderivCLM_apply Nat.cast_zero LT.lt.trans_le ENat.add_one_pos DifferentiableAt.lineDeriv_eq_fderiv Differentiable.differentiableAt ContDiff.differentiable contDiff LT.lt.ne'
lineDerivCLM_apply_of_gt 📖	mathematical	ENat instLTENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	lineDerivCLM ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction 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.zero	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ext lineDerivCLM_apply not_le_of_gt
lineDerivCLM_apply_of_le 📖	mathematical	ENat instLEENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	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 lineDerivCLM lineDeriv DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul lineDerivCLM_apply
lineDerivCLM_eq_fderivCLM 📖	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 lineDerivCLM Real.semiring ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids Real.normedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Real.commRing ContinuousLinearMap.module SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup fderivCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
lineDerivCLM_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 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 lineDerivCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
lineDerivCLM_smul 📖	mathematical	—	lineDerivCLM Real 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 Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction topologicalSpace AddCommGroup.toAddCommMonoid instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul IsScalarTower.to_smulCommClass Real.instCommSemiring UniformContinuousConstSMul.to_continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero 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.instSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing Real.commRing Real.pseudoMetricSpace Real.instZero IsScalarTower.to_smulCommClass' CommSemiring.toSemiring instIsScalarTower Algebra.toSMul ContinuousSMul.continuousConstSMul instContinuousSMulReal	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self IsScalarTower.to_smulCommClass' instIsScalarTower ContinuousSMul.continuousConstSMul instContinuousSMulReal ext RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup fderivCLM_apply map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
lineDerivOpCLM_eq_lineDerivCLM 📖	mathematical	—	LineDeriv.lineDerivOpCLM TestFunction Top.top ENat instTopENat NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instAddCommGroup instModuleOfSMulCommClassRealOfContinuousConstSMul Ring.toSemiring NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup IsScalarTower.to_smulCommClass Real Real.instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField 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 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 topologicalSpace instLineDerivTopENat instLineDerivAddTopENat instLineDerivSMulTopENat instContinuousLineDerivTopENat lineDerivCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul instLineDerivAddTopENat instLineDerivSMulTopENat instContinuousLineDerivTopENat
lineDerivOp_eq_lineDerivCLM 📖	mathematical	—	LineDeriv.lineDerivOp TestFunction Top.top ENat instTopENat instLineDerivTopENat DFunLike.coe 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 lineDerivCLM	—	—
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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction 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 mkCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
monoCLM_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 monoCLM ENat instLEENat TopologicalSpace.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder LinearOrder.toDecidableLE instLinearOrderENat instZero	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul instIsTopologicalAddGroup instContinuousSMulReal instLocallyConvexSpaceReal hasCompactSupport monoCLM.eq_1 limitCLM.congr_simp
monoCLM_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 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 monoCLM	—	IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul
monoCLM_eq_zero 📖	mathematical	ENat instLEENat TopologicalSpace.Opens UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	monoCLM ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TestFunction 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.zero	—	ContinuousLinearMap.ext IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ext monoCLM_apply
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 ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid 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 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 ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid 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 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	30 math math: instContinuousMapClass, TestFunction.lineDerivCLM_apply_of_le, Distribution.delta_apply, TestFunction.ext_iff, TestFunction.coe_neg, TestFunction.toBoundedContinuousFunctionCLM_apply, TestFunction.fderivCLM_apply_of_le, TestFunction.contDiff, TestFunction.coe_smul, TestFunction.postcompCLM_apply, instBoundedContinuousMapClass, TestFunction.instContinuousEval, map_hasCompactSupport, TestFunction.lineDerivCLM_eq_fderivCLM, TestFunction.lineDerivCLM_apply, TestFunction.coe_add, TestFunction.coe_zero, TestFunction.tsupport_subset, TestFunction.coe_sub, TestFunction.coe_ofSupportedIn, TestFunction.toFun_eq_coe, TestFunction.monoCLM_apply, TestFunction.coe_copy, TestFunction.hasCompactSupport, TestFunction.fderivCLM_apply, 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	58 math math: TestFunction.lineDerivCLM_apply_of_le, Distribution.delta_apply, TestFunction.ext_iff, TestFunction.coe_neg, TestFunction.toBoundedContinuousFunctionCLM_eq_of_scalars, TestFunction.monoCLM_eq_zero, TestFunction.continuous_iff_continuous_comp, TestFunction.toBoundedContinuousFunctionCLM_apply, TestFunction.instIsUniformAddGroup, TestFunction.fderivCLM_apply_of_le, TestFunction.lineDerivOpCLM_eq_lineDerivCLM, TestFunction.fderivCLM_ofSupportedIn, TestFunction.contDiff, TestFunction.continuous_ofSupportedIn, TestFunction.limitCLM_apply, TestFunction.instContinuousLineDerivTopENat, TestFunction.instIsScalarTower, TestFunction.instIsTopologicalAddGroup, TestFunction.coe_smul, TestFunction.postcompCLM_apply, Distribution.delta_eq_zero_of_notMem, TestFunction.coe_ofSupportedInCLM, TestFunction.instLineDerivAddTopENat, TestFunction.instContinuousEval, TestFunction.coe_ofSupportedInLM, TestFunction.lineDerivCLM_add, Distribution.mapCLM_apply, TestFunction.lineDerivOp_eq_lineDerivCLM, TestFunction.lineDerivCLM_eq_fderivCLM, TestFunction.lineDerivCLM_apply, TestFunction.coe_add, TestFunction.coe_zero, TestFunction.instLineDerivLeftSMulRealTopENat, TestFunction.monoCLM_eq_of_scalars, TestFunction.tsupport_subset, TestFunction.coe_sub, TestFunction.mkCLM_apply, TestFunction.fderivCLM_eq_of_scalars, TestFunction.lineDerivCLM_eq_of_scalars, TestFunction.coe_ofSupportedIn, TestFunction.fderivCLM_apply_of_gt, TestFunction.lineDerivCLM_smul, TestFunction.toFun_eq_coe, TestFunction.monoCLM_apply, TestFunction.instLocallyConvexSpaceReal, TestFunction.coe_copy, TestFunction.instLineDerivSMulTopENat, TestFunction.hasCompactSupport, TestFunction.fderivCLM_apply, TestFunction.coe_toBoundedContinuousFunction, TestFunction.instContinuousSMulReal, TestFunction.lineDerivCLM_apply_of_gt, TestFunction.instT3Space, TestFunction.coeFnAddMonoidHom_apply, TestFunction.topologicalSpace_le_iff, TestFunction.injective_toBoundedContinuousFunctionCLM, TestFunction.coe_mk, TestFunction.originalTop_le
TestFunctionClass 📖	CompData	—

---

← Back to Index