StrongTopology

📁 Source: Mathlib/Topology/Algebra/Module/StrongTopology.lean

Statistics

Metric	Count
Definitions CompactConvergenceCLM, «term_→L_c[_]_», «term_→SL_c[_]_», arrowCongr, arrowCongrSL, conjContinuousAlgEquiv, coprodEquivL, postcomp, postcompCompactConvergenceCLM, postcompUniformConvergenceCLM, postcomp_uniformConvergenceCLM, precomp, precompCompactConvergenceCLM, precompUniformConvergenceCLM, precomp_uniformConvergenceCLM, prodL, restrictScalarsL, toBilinForm, toLinearMap₁₂, toSpanSingletonCLE, toUniformConvergenceCLM, topologicalSpace, uniformSpace, UniformConvergenceCLM, instAddCommGroup, instDistribMulAction, instFunLike, instModule, instTopologicalSpace, instUniformSpace, postcomp_compactConvergenceCLM, precomp_compactConvergenceCLM	32
Theorems continuousSMul, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, instContinuousEvalConst, instT2Space, arrowCongrSL_apply, arrowCongrSL_symm_apply, arrowCongrSL_toLinearEquiv_apply, arrowCongrSL_toLinearEquiv_symm_apply, arrowCongr_apply, arrowCongr_symm, conjContinuousAlgEquiv_apply, conjContinuousAlgEquiv_apply_apply, conjContinuousAlgEquiv_refl, conjContinuousAlgEquiv_trans, symm_conjContinuousAlgEquiv, symm_conjContinuousAlgEquiv_apply_apply, coe_restrictScalarsL, coe_restrict_scalarsL', completeSpace, continuousConstSMul, continuousSMul, continuous_restrictScalars, coprodEquivL_apply_apply, coprodEquivL_symm_apply, eventually_nhds_zero_mapsTo, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, instCompleteSpace, instContinuousEvalConst, instT2Space, isEmbedding_postcomp, isEmbedding_restrictScalars, isInducing_postcomp, isUniformAddGroup, isUniformEmbedding_postcomp, isUniformEmbedding_restrictScalars, isUniformEmbedding_toUniformOnFun, isUniformInducing_postcomp, isVonNBounded_iff, isVonNBounded_image2_apply, map_add₂, map_neg₂, map_smul₂, map_smulₛₗ₂, map_sub₂, map_zero₂, nhds_zero_eq, nhds_zero_eq_of_basis, postcompCompactConvergenceCLM_apply, postcompUniformConvergenceCLM_apply, postcomp_apply, postcomp_uniformConvergenceCLM_apply, precompCompactConvergenceCLM_apply, precompUniformConvergenceCLM_apply, precomp_apply, precomp_uniformConvergenceCLM_apply, prodL_apply, toBilinForm_apply, toBilinForm_inj, toBilinForm_injective, toLinearMap₁₂_apply, toLinearMap₁₂_inj, toLinearMap₁₂_injective, toSpanSingletonCLE_apply_apply, toSpanSingletonCLE_symm_apply, toUniformConvergenceCLM_apply, toUniformConvergenceCLM_continuous, toUniformConvergenceCLM_symm_apply, topologicalAddGroup, uniformContinuousConstSMul, uniformContinuous_restrictScalars, add_apply, coe_zero, completeSpace, continuousEvalConst, continuousSMul, eventually_nhds_zero_mapsTo, ext, ext_iff, hasBasis_nhds_zero, hasBasis_nhds_zero_of_basis, instContinuousConstSMul, instContinuousSemilinearMapClass, instIsTopologicalAddGroup, instIsUniformAddGroup, instUniformContinuousConstSMul, isEmbedding_coeFn, isUniformEmbedding_coeFn, isUniformEmbedding_postcomp, isUniformInducing_coeFn, isUniformInducing_postcomp, isVonNBounded_iff, isVonNBounded_image2_apply, neg_apply, nhds_zero_eq, nhds_zero_eq_of_basis, smul_apply, sub_apply, sum_apply, t2Space, tendsto_iff_tendstoUniformlyOn, topologicalSpace_eq, topologicalSpace_mono, uniformSpace_eq, uniformSpace_mono, uniformity_toTopologicalSpace_eq, postcomp_compactConvergenceCLM_apply, precomp_compactConvergenceCLM_apply	109
Total	141

CompactConvergenceCLM

Definitions

Name	Category	Theorems
«term_→L_c[_]_» 📖	CompOp	—
«term_→SL_c[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul CompactConvergenceCLM UniformSpace.toTopologicalSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup setOf Set IsCompact DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformConvergenceCLM.instDistribMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing UniformConvergenceCLM.instTopologicalSpace	—	UniformConvergenceCLM.continuousSMul TotallyBounded.isVonNBounded IsCompact.totallyBounded
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis CompactConvergenceCLM Set nhds UniformConvergenceCLM.instTopologicalSpace setOf IsCompact NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid UniformConvergenceCLM.instAddCommGroup Filter Filter.instMembership	—	hasBasis_nhds_zero_of_basis Filter.basis_sets
hasBasis_nhds_zero_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CompactConvergenceCLM Set UniformConvergenceCLM.instTopologicalSpace setOf IsCompact UniformConvergenceCLM.instAddCommGroup	—	UniformConvergenceCLM.hasBasis_nhds_zero_of_basis isCompact_empty directedOn_of_sup_mem IsCompact.union
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst CompactConvergenceCLM UniformConvergenceCLM.instFunLike setOf Set IsCompact UniformConvergenceCLM.instTopologicalSpace	—	UniformConvergenceCLM.continuousEvalConst Set.sUnion_isCompact_eq_univ
instT2Space 📖	mathematical	—	T2Space CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact	—	UniformConvergenceCLM.t2Space Set.sUnion_isCompact_eq_univ

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
arrowCongr 📖	CompOp	13 math math: MDifferentiableAt.cle_arrowCongr, MDifferentiable.cle_arrowCongr, arrowCongr_apply, MDifferentiableWithinAt.cle_arrowCongr, arrowCongr_symm, ContMDiffOn.cle_arrowCongr, MDifferentiableOn.cle_arrowCongr, fderiv_continuousLinearEquiv_comp, fderivWithin_continuousLinearEquiv_comp, ContMDiffWithinAt.cle_arrowCongr, fderiv_continuousLinearEquiv_comp', ContMDiffAt.cle_arrowCongr, ContMDiff.cle_arrowCongr
arrowCongrSL 📖	CompOp	4 math math: arrowCongrSL_apply, arrowCongrSL_symm_apply, arrowCongrSL_toLinearEquiv_apply, arrowCongrSL_toLinearEquiv_symm_apply
conjContinuousAlgEquiv 📖	CompOp	9 math math: conjContinuousAlgEquiv_refl, conjContinuousAlgEquiv_surjective, conjContinuousAlgEquiv_apply, conjContinuousAlgEquiv_trans, ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv, conjContinuousAlgEquiv_ext_iff, symm_conjContinuousAlgEquiv, conjContinuousAlgEquiv_apply_apply, symm_conjContinuousAlgEquiv_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowCongrSL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap symm	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongrSL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike symm arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongrSL_toLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike toLinearEquiv ContinuousLinearMap.topologicalSpace IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap symm	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongrSL_toLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommMonoid ContinuousLinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm toLinearEquiv ContinuousLinearMap.topologicalSpace IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing arrowCongrSL ContinuousLinearMap.comp toContinuousLinearMap symm	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongr_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike ContinuousLinearEquiv RingHomInvPair.ids ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike equivLike arrowCongr symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
arrowCongr_symm 📖	mathematical	—	symm DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap AddCommGroup.toAddCommMonoid ContinuousLinearMap.topologicalSpace ContinuousLinearMap.addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing arrowCongr	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
conjContinuousAlgEquiv_apply 📖	mathematical	—	DFunLike.coe ContinuousAlgEquiv ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousAlgEquiv.equivLike conjContinuousAlgEquiv ContinuousLinearMap.comp RingHomCompTriple.ids toContinuousLinearMap RingHomInvPair.ids symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
conjContinuousAlgEquiv_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike ContinuousAlgEquiv Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousAlgEquiv.equivLike conjContinuousAlgEquiv ContinuousLinearEquiv RingHomInvPair.ids equivLike symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
conjContinuousAlgEquiv_refl 📖	mathematical	—	conjContinuousAlgEquiv refl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousAlgEquiv.refl ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
conjContinuousAlgEquiv_trans 📖	mathematical	—	conjContinuousAlgEquiv trans DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids AddCommGroup.toAddCommMonoid ContinuousAlgEquiv.trans ContinuousLinearMap Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left RingHomCompTriple.ids
symm_conjContinuousAlgEquiv 📖	mathematical	—	ContinuousAlgEquiv.symm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero conjContinuousAlgEquiv symm RingHomInvPair.ids	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left
symm_conjContinuousAlgEquiv_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike ContinuousAlgEquiv Semifield.toCommSemiring ContinuousLinearMap.semiring IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup ContinuousLinearMap.topologicalSpace ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousAlgEquiv.equivLike ContinuousAlgEquiv.symm conjContinuousAlgEquiv ContinuousLinearEquiv RingHomInvPair.ids equivLike symm	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsScalarTower.left

ContinuousLinearMap

Definitions

Name	Category	Theorems
coprodEquivL 📖	CompOp	2 math math: coprodEquivL_apply_apply, coprodEquivL_symm_apply
postcomp 📖	CompOp	10 math math: MDifferentiableOn.clm_postcomp, ContMDiffOn.clm_postcomp, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, MDifferentiable.clm_postcomp, MDifferentiableAt.clm_postcomp, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, postcomp_apply, ContMDiff.clm_postcomp, MDifferentiableWithinAt.clm_postcomp
postcompCompactConvergenceCLM 📖	CompOp	2 math math: postcompCompactConvergenceCLM_apply, postcomp_compactConvergenceCLM_apply
postcompUniformConvergenceCLM 📖	CompOp	2 math math: postcompUniformConvergenceCLM_apply, postcomp_uniformConvergenceCLM_apply
postcomp_uniformConvergenceCLM 📖	CompOp	—
precomp 📖	CompOp	9 math math: MDifferentiableWithinAt.clm_precomp, ContMDiffOn.clm_precomp, ContMDiffAt.clm_precomp, MDifferentiableAt.clm_precomp, MDifferentiableOn.clm_precomp, MDifferentiable.clm_precomp, ContMDiffWithinAt.clm_precomp, ContMDiff.clm_precomp, precomp_apply
precompCompactConvergenceCLM 📖	CompOp	2 math math: precomp_compactConvergenceCLM_apply, precompCompactConvergenceCLM_apply
precompUniformConvergenceCLM 📖	CompOp	2 math math: precompUniformConvergenceCLM_apply, precomp_uniformConvergenceCLM_apply
precomp_uniformConvergenceCLM 📖	CompOp	—
prodL 📖	CompOp	1 math math: prodL_apply
restrictScalarsL 📖	CompOp	4 math math: bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, coe_restrict_scalarsL', coe_restrictScalarsL, bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp
toBilinForm 📖	CompOp	7 math math: ProbabilityTheory.isGaussian_iff_gaussian_charFun, toBilinForm_apply, toBilinForm_inj, ProbabilityTheory.isPosSemidef_covarianceBilin, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, toBilinForm_injective, ProbabilityTheory.isPosSemidef_covarianceBilinDual
toLinearMap₁₂ 📖	CompOp	19 math math: toLinearMap₁₂_injective, toLinearMap₁₂_apply, VectorFourier.fourierIntegral_continuousLinearMap_apply, VectorFourier.hasFDerivAt_fourierIntegral, VectorFourier.fourierIntegral_iteratedFDeriv, VectorFourier.differentiable_fourierIntegral, VectorFourier.iteratedFDeriv_fourierIntegral, toLinearMap₁₂_inj, VectorFourier.fderiv_fourierIntegral, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', VectorFourier.contDiff_fourierIntegral, Real.fourierIntegral_continuousLinearMap_apply', VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, VectorFourier.fourierIntegral_continuousMultilinearMap_apply, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, VectorFourier.fourierIntegral_fderiv, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, Real.fourierIntegral_continuousMultilinearMap_apply'
toSpanSingletonCLE 📖	CompOp	2 math math: toSpanSingletonCLE_apply_apply, toSpanSingletonCLE_symm_apply
toUniformConvergenceCLM 📖	CompOp	3 math math: toUniformConvergenceCLM_apply, toUniformConvergenceCLM_continuous, toUniformConvergenceCLM_symm_apply
topologicalSpace 📖	CompOp	523 math math: ContMDiffAt.coordChangeL, instT2Space, MDifferentiable.coordChangeL, ContinuousLinearEquiv.conjContinuousAlgEquiv_refl, LinearMap.mkContinuous₂_norm_le', derivWithin_of_bilinear, Bundle.ContMDiffRiemannianMetric.isVonNBounded, LinearMap.mkContinuous₂_apply, isPositive_iff_eq_sum_rankOne, Bundle.ContMDiffRiemannianMetric.contMDiff, continuousOn_stereoToFun, InnerProductSpace.isPositive_rankOne_self, ProbabilityTheory.isGaussian_iff_gaussian_charFun, mulLeftRight_isBoundedBilinear, analyticWithinAt_bilinear, HasCompactSupport.convolution_integrand_bound_left, compSL_apply, continuous₂, SchwartzMap.integral_sesq_fourier_fourier, Real.hasFDerivAt_fourierChar_neg_bilinear_left, MeasureTheory.convolution_eq_right', InnerProductSpace.rankOne_one_left_eq_innerSL, continuous_det, map_add_add, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, fderivWithin_fderivWithin_eq_of_mem_nhdsWithin, toLinearMap₁₂_injective, ProbabilityTheory.covarianceBilinDual_apply', continuousSMul, ContinuousMultilinearMap.analyticAt_uncurry_of_linear, SchwartzMap.pairing_apply_apply, InnerProductSpace.isIdempotentElem_rankOne_self, ProbabilityTheory.covarianceBilinDual_apply, Real.fderiv_fourierChar_neg_bilinear_right_apply, Continuous.convolution_integrand_fst, iteratedFDerivWithin_succ_eq_comp_right, innerSL_apply_apply, SchwartzMap.integral_bilin_fourierInv_eq, ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap, ContMDiffWithinAt.mfderivWithin_const, innerSL_apply_comp_of_isSymmetric, Unitization.splitMul_apply, toBilinForm_apply, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, ProbabilityTheory.uncenteredCovarianceBilin_apply, mdifferentiableOn_symm_coordChangeL, opNorm_lsmul_apply_le, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, SchwartzMap.bilinLeftCLM_apply, fpowerSeriesBilinear_apply_zero, fderiv_continuousAlternatingMap_apply_const, nhds_zero_eq_of_basis, Bundle.RiemannianMetric.isVonNBounded, ContinuousMultilinearMap.norm_compContinuousLinearMapLRight_le, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, Differentiable.fderiv_norm_rpow, integrable_of_bilin_of_bdd_left, isometry_mul_flip, ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective, HasFDerivWithinAt.linear_multilinear_comp, CStarModule.innerSL_apply, hasDerivWithinAt_of_bilinear, Bundle.ContinuousLinearMap.vectorBundle, contDiff_one_iff_fderiv, MeasureTheory.ConvolutionExistsAt.integrable, opNorm_mul_flip_apply, bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars, InnerProductSpace.inner_left_rankOne_apply, Pretrivialization.continuousLinearMap_symm_apply', HasFDerivAt.norm_sq, hasBasis_nhds_zero, ContDiffAt.continuousAt_fderiv, Real.integrable_prod_sub, topologicalAddGroup, HasFDerivAt.continuousMultilinear_apply_const, InnerProductSpace.rankOne_apply, NormedSpace.Dual.toWeakDual_continuous, MeasureTheory.convolution_integrand_bound_right_of_le_of_subset, ContinuousMultilinearMap.norm_smulRightL_le, precompL_apply, VectorBundleCore.contMDiffOn_coordChange, toSesqForm_apply_coe, SchwartzMap.integral_bilin_fourierIntegral_eq, toLinearMap₁₂_apply, NormedSpace.isClosed_polar, VectorFourier.fourierPowSMulRight_eq_comp, hasFDerivWithinAt_of_bilinear, opNorm_mul, flipMultilinear_apply_apply, compactOperator_topologicalClosure, isEmbedding_postcomp, SchwartzMap.integral_sesq_fourier_eq, adjointAux_norm, ProbabilityTheory.covarianceBilin_apply_basisFun_self, hasStrictFDerivAt_of_bilinear, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply, Real.fourier_iteratedFDeriv, mulLeftRight_apply, Bundle.ContinuousRiemannianMetric.symm, ContinuousMultilinearMap.curryRight_norm, analyticOn_bilinear, coe_innerSL_apply, RegularNormedAlgebra.isometry_mul', hasFDerivAt_ringInverse, contDiffAt_one_iff, VectorFourier.fourierIntegral_iteratedFDeriv, InnerProductSpace.nnnorm_rankOne, ContinuousLinearEquiv.arrowCongr_apply, flip_smul, InnerProductSpace.isSymmetricProjection_rankOne_self, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, MeasureTheory.ConvolutionExistsAt.integrable_swap, continuousOn_tangentCoordChange, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, instLocallyConvexSpace, NormedSpace.inclusionInDoubleDual_norm_eq, ContinuousLinearEquiv.conjContinuousAlgEquiv_trans, fderiv_of_bilinear, tendsto_integral_exp_smul_cocompact, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, opNorm_mul_apply, norm_smulRightL, MeasureTheory.convolution_def, Pretrivialization.continuousLinearMapCoordChange_apply, InnerProductSpace.trace_rankOne, ContMDiffVectorBundle.continuousLinearMap, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, continuous_restrictScalars, hasFDerivAt_norm_rpow, compL_apply, lsmul_flip_inj, summable_jacobiTheta₂_term_fderiv_iff, inCoordinates_apply_eq₂, flip_apply, ProbabilityTheory.covarianceBilin_zero, contDiffOn_stereoToFun, fderiv_inverse, bilinearRestrictScalars_apply_apply, InnerProductSpace.adjoint_rankOne, InnerProductSpace.rankOne_eq_zero, Real.fourierIntegral_convergent_iff', Bundle.ContMDiffRiemannianMetric.symm, ContMDiffOn.coordChangeL, InnerProductSpace.inner_right_rankOne_apply, SchwartzMap.pairing_apply, ContDiff.continuous_fderiv, mdifferentiableAt_hom_bundle, innerSL_inj, fderivWithin_inv', StrongDual.toLp_of_not_memLp, fderivWithin_of_bilinear, NormedSpace.inclusionInDoubleDual_norm_le, InnerProductSpace.rankOne_eq_rankOne_iff_comm, precompR_apply, ContinuousAlternatingMap.norm_alternatizeUncurryFinCLM_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd', ProbabilityTheory.IsGaussian.charFun_eq', ProbabilityTheory.covarianceBilinDual_eq_covariance, ContMDiffAt.mfderiv_const, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, ProbabilityTheory.covarianceBilinDual_zero, Continuous.fderiv, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, hasStrictDerivAt_of_bilinear, ContinuousLinearEquiv.arrowCongr_symm, isBoundedBilinearMap, fderivWithin_continuousMultilinear_apply_const, Differentiable.fderiv_two, instContinuousEvalConst, MDifferentiableOn.coordChangeL, continuousMultilinearCurryRightEquiv_symm_apply, lsmul_apply, Bundle.ContMDiffRiemannianMetric.pos, bilinearComp_zero_right, IsContMDiffRiemannianBundle.exists_contMDiff, InnerProductSpace.rank_rankOne, contMDiffAt_coordChangeL, adjointAux_apply, ProperCone.innerDual_singleton, InnerProductSpace.rankOne_def, MDifferentiableWithinAt.coordChangeL, coe_flipₗᵢ', stereoToFun_apply, adjointAux_inner_left, hasSum_jacobiTheta₂_term_fderiv, fderivWithin_fderivWithin_eq_of_mem_nhds, ProbabilityTheory.covarianceBilin_comm, SchwartzMap.integral_bilin_fourier_eq, ClosedSubmodule.orthogonal_eq_inter, coe_flipMultilinearEquiv, NonUnitalAlgHom.coe_Lmul, ContinuousMultilinearMap.norm_map_init_le, SchwartzMap.smulRightCLM_apply_apply, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin, ContDiffWithinAt.continuousWithinAt_fderivWithin, coe_restrict_scalarsL', fderivWithin_fderivWithin_eq_of_eventuallyEq, norm_iteratedFDeriv_le_of_bilinear, ContinuousMultilinearMap.cpolyomialOn_uncurry_of_linear, aestronglyMeasurable_comp₂, HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt, norm_precompR_le, hasFPowerSeriesOnBall_bilinear, eventually_nhds_zero_mapsTo, deriv_of_bilinear, Orientation.areaForm'_apply, innerSLFlip_apply_apply, nnnorm_holder_apply_apply_le, bilinear_hasTemperateGrowth, IsContinuousRiemannianBundle.exists_continuous, ContinuousAlternatingMap.fderivCompContinuousLinearMap_eq_alternatizeUncurryFin, postcomp_apply, prodMapL_apply, ContinuousLinearEquiv.nhds, contMDiffOn_continuousLinearMapCoordChange, InnerProductSpace.enorm_rankOne, InnerProductSpace.continuousLinearMapOfBilin_zero, ContinuousMultilinearMap.compContinuousLinearMapLRight_apply, toLinearMap_innerSL_apply, ContinuousMultilinearMap.flipLinear_apply_apply, VectorFourier.integral_sesq_fourierIntegral_eq_neg_flip, HasFDerivWithinAt.norm_sq, uncurryBilinear_apply, VectorBundle.continuousOn_coordChange', MeasureTheory.integral_posConvolution, VectorFourier.integral_fourierIntegral_swap, Bundle.RiemannianMetric.symm, Unitization.norm_eq_sup, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd', ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff, iteratedFDerivWithin_two_apply', memLp_of_bilin, ProbabilityTheory.covarianceBilin_self_nonneg, HasStrictFDerivAt.continuousMultilinear_apply_const, opNorm_mulLeftRight_apply_le, analyticOnNhd_bilinear, ProbabilityTheory.covarianceBilinDual_self_eq_variance, hasStrictFDerivAt_norm_sq, fderiv_tsum, ContinuousMultilinearMap.cpolynomialAt_uncurry_of_linear, map_sub₂, bilinearComp_apply, tendsto_integral_exp_smul_cocompact_of_inner_product, Trivialization.baseSet_continuousLinearMap, contMDiffOn_symm_coordChangeL, contMDiffAt_hom_bundle, HasFDerivAt.continuousAlternatingMap_apply_const, ProbabilityTheory.covarianceBilinDual_self_nonneg, ContinuousAlternatingMap.fderivCompContinuousLinearMapCLM_apply, adjointAux_adjointAux, ProbabilityTheory.covarianceBilin_real_self, coprodEquivL_apply_apply, flip_add, continuous_clm_apply, VectorFourier.fourierSMulRight_apply, ContinuousMultilinearMap.uncurryRight_apply, isVonNBounded_iff, bilinearComp_zero, Trivialization.continuousLinearMap_apply, ContinuousAlternatingMap.toContinuousMultilinearMapCLM_comp_fderivCompContinuousLinearMap, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, Real.fourier_bilin_convolution_eq, hom_trivializationAt, le_opNorm₂, lpPairing_eq_integral, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, InnerProductSpace.rankOne_def', opNorm_mul_le, Pretrivialization.continuousLinearMap.isLinear, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, ContDiffOn.continuousOn_fderivWithin, SchwartzMap.integral_sesq_fourierIntegral_eq, MeasureTheory.Integrable.convolution_integrand, ProbabilityTheory.covarianceBilin_apply_pi, SchwartzMap.integral_bilinear_laplacian_right_eq_left, isometry_mul, isOpen_injective, MeasureTheory.dist_convolution_le', isInducing_postcomp, InnerProductSpace.innerSL_norm, ContinuousMultilinearMap.curryRight_apply, ContMDiffWithinAt.mfderivWithin, VectorPrebundle.exists_coordChange, ProbabilityTheory.covarianceBilin_apply_basisFun, ContinuousMultilinearMap.analyticOn_uncurry_of_linear, mdifferentiableOn_continuousLinearMapCoordChange, InnerProductSpace.isStarProjection_rankOne_self, LinearMap.mkContinuous₂_norm_le, MeasureTheory.AEStronglyMeasurable.fourierSMulRight, hasFPowerSeriesAt_bilinear, continuousConstSMul, PiTensorProduct.mapLMultilinear_apply_apply, hasStrictFDerivAt_ringInverse, ContDiffOn.continuousOn_fderiv_of_isOpen, mul_apply', InnerProductSpace.rankOne_comp_rankOne, InnerProductSpace.rankOne_comp, hasBasis_nhds_zero_of_basis, InnerProductSpace.toMatrix_rankOne, HasFDerivWithinAt.continuousMultilinear_apply_const, InnerProductSpace.isSymmetric_rankOne_self, opNNNorm_mul, norm_iteratedFDerivWithin_le_of_bilinear, iteratedFDeriv_succ_eq_comp_right, fderiv_continuousLinearEquiv_comp, adjoint_toSpanSingleton, toBilinForm_injective, ProbabilityTheory.isPosSemidef_covarianceBilinDual, isEmbedding_restrictScalars, IsBoundedBilinearMap.toContinuousLinearMap_apply, hom_trivializationAt_source, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, innerSLFlip_apply, ProbabilityTheory.covarianceBilin_real, mdifferentiableOn_coordChangeL, opNorm_mulLeftRight_apply_apply_le, opNorm_lsmul_le, ProbabilityTheory.covarianceBilin_of_not_memLp, innerSL_apply_norm, Real.fourier_bilin_convolution_eq_integral, coe_restrictScalarsL, norm_compL_le, ContinuousMultilinearMap.hasStrictFDerivAt_compContinuousLinearMap, ContMDiffVectorBundle.contMDiffOn_coordChangeL, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, fderiv_continuousMultilinear_apply_const, ProbabilityTheory.covarianceBilinDual_comm, opNNNorm_mul_flip_apply, MDifferentiableAt.coordChangeL, fderivWithin_continuousAlternatingMap_apply_const, ContinuousLinearEquiv.arrowCongrSL_apply, Pretrivialization.continuousLinearMap_apply, hasFDerivAt_uncurry_of_multilinear, opNorm_mul_apply_le, contDiff_one_iff_hasFDerivAt, ProbabilityTheory.covarianceBilin_apply, HasFDerivAt.linear_multilinear_comp, MeasureTheory.convolutionExistsAt_iff_integrable_swap, hasFDerivAt_tsum, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, norm_bilinearRestrictScalars, nhds_zero_eq, ContinuousMultilinearMap.analyticWithinAt_uncurry_of_linear, ProbabilityTheory.covarianceBilin_map, Unitization.nnnorm_eq_sup, bilinearComp_zero_left, Bundle.ContinuousRiemannianMetric.pos, IsCoercive.continuousLinearEquivOfBilin_apply, VectorBundleCore.continuousOn_coordChange, VectorFourier.integral_bilin_fourierIntegral_eq_flip, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, InnerProductSpace.toLinearMap_rankOne, instSecondCountableTopologyContinuousLinearMapIdOfFiniteDimensional, adjointAux_inner_right, Bundle.RiemannianMetric.pos, ContinuousLinearEquiv.isOpen, continuousMultilinearCurryRightEquiv_symm_apply', ContinuousAlternatingMap.fderivCompContinuousLinearMap_apply, prodL_apply, iteratedFDerivWithin_two_apply, Pretrivialization.continuousOn_continuousLinearMapCoordChange, DoubleCentralizer.coe_fst, hasFDerivAt_of_bilinear, ProbabilityTheory.uncenteredCovarianceBilin_zero, VectorFourier.fourierPowSMulRight_apply, opNorm_flip, continuousOn_integral_bilinear_of_locally_integrable_of_compact_support, VectorPrebundle.continuousOn_coordChange, tendsto_of_tendsto_pointwise_of_cauchySeq, FormalMultilinearSeries.derivSeries_eq_zero, ContMDiffWithinAt.coordChangeL, norm_compSL_le, innerSL_apply, SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left, InnerProductSpace.isIdempotentElem_rankOne_self_iff, fderivWithin_continuousLinearEquiv_comp, Pretrivialization.continuousLinearMap_symm_apply, StrongDual.toLp_apply, map_smul₂, coe_flipₗᵢ, ContinuousAlternatingMap.fderivCompContinuousLinearMap_of_isEmpty, ContMDiffAt.mfderiv, continuousAt_hom_bundle, VectorPrebundle.contMDiffOn_contMDiffCoordChange, Real.differentiable_fourierChar_neg_bilinear_right, OrthonormalBasis.sum_rankOne_eq_id, mdifferentiableAt_coordChangeL, HasStrictFDerivAt.continuousAlternatingMap_apply_const, norm_smulRightL_le, coe_symm_flipMultilinearEquiv, VectorFourier.norm_fourierSMulRight_le, continuousWithinAt_hom_bundle, signedDist_apply, continuousMultilinearCurryRightEquiv_apply', flipₗᵢ'_symm, flip_zero, VectorFourier.norm_fourierPowSMulRight_le, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, Real.hasFDerivAt_fourierChar_neg_bilinear_right, VectorFourier.norm_fourierSMulRight, hom_chart, toUniformConvergenceCLM_continuous, hasStrictFDerivAt_inv', iteratedFDeriv_two_apply, hom_trivializationAt_apply, Real.differentiable_fourierChar_neg_bilinear_left, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, ContinuousMultilinearMap.smulRightL_apply, instBorelSpace, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, contMDiffOn_coordChangeL, ContinuousLinearEquiv.arrowCongrSL_symm_apply, opNorm_mulLeftRight_le, MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound, hom_trivializationAt_baseSet, Submodule.orthogonal_eq_inter, lsmul_flip_apply, compContinuousAlternatingMapCLM_apply_apply, fderiv_norm_rpow, map_add₂, Bundle.ContinuousLinearMap.memTrivializationAtlas, FormalMultilinearSeries.derivSeries_apply_diag, opNorm_lsmul, ProbabilityTheory.covarianceBilinDual_of_not_memLp, ContinuousMultilinearMap.fderivCompContinuousLinearMap_apply, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv, InnerProductSpace.continuousLinearMapOfBilin_apply, NormedSpace.double_dual_bound, MeasureTheory.convolution_eq_swap, map_zero₂, Real.zero_at_infty_vector_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, precomp_apply, norm_holderL_le, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound, analyticAt_bilinear, ProbabilityTheory.IsGaussian.charFunDual_eq', toPointwiseConvergenceCLM_apply, innerSL_apply_coe, bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp, hasFDerivAt_inv', exists_continuousLinearEquiv_fderiv_symm_eq, MeasureTheory.AEStronglyMeasurable.convolution_integrand', map_neg₂, Bundle.RiemannianMetric.continuousAt, holderL_apply_apply, MeasureTheory.AEStronglyMeasurable.convolution_integrand, norm_innerSL_le, VectorFourier.hasFDerivAt_fourierChar_smul, continuousMultilinearCurryRightEquiv_apply, integrable_of_bilin_of_bdd_right, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply, apply_apply', ProbabilityTheory.covarianceBilinDual_of_not_memLp', ContinuousMultilinearMap.analyticOnNhd_uncurry_of_linear, flipₗᵢ_symm, exists_continuousLinearEquiv_fderivWithin_symm_eq, norm_holder_apply_apply_le, fderiv_continuousLinearEquiv_comp', smulRightL_apply_apply, continuousOn_clm_apply, ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT, toSpanSingletonCLE_apply_apply, opNNNorm_mul_apply, toSpanSingletonCLE_symm_apply, mdifferentiableWithinAt_hom_bundle, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, norm_precompL_le, Real.fderiv_fourierChar_neg_bilinear_left_apply, apply_apply, ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear_apply_apply, IsSymmSndFDerivWithinAt.eq, map_smulₛₗ₂, PiTensorProduct.mapLMultilinear_opNorm, hasFDerivAt_tsum_of_isPreconnected, Real.fourierIntegral_iteratedFDeriv, hom_trivializationAt_target, ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply, MeasureTheory.AEStronglyMeasurable.convolution_integrand_swap_snd, HasCompactSupport.convolution_integrand_bound_right, ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply, InnerProductSpace.symm_toEuclideanLin_rankOne, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, adjoint_innerSL_apply, fderiv_tsum_apply, coprodEquivL_symm_apply, continuousOn_coordChange, HasCompactSupport.convolution_integrand_bound_right_of_subset, contMDiffWithinAt_hom_bundle, mem_contMDiffFiberwiseLinear_iff, norm_smulRightL_apply, isOpen_setOf_nat_le_rank, isClosed_setOf_isCompactOperator, DoubleCentralizer.coe_snd, fpowerSeriesBilinear_apply_one, MeasureTheory.integral_convolution, fderiv_norm_sq_apply, NormedSpace.dual_def, fderiv_norm_sq, coe_mulₗᵢ, HasFDerivWithinAt.continuousAlternatingMap_apply_const, innerSL_apply_comp, toSesqForm_apply_norm_le, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd, coeFn_holder, coe_deriv₂, ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply, ContinuousAlternatingMap.alternatizeUncurryFinCLM_apply, Bundle.ContinuousRiemannianMetric.isVonNBounded, hasDerivAt_of_bilinear, ContMDiff.coordChangeL, InnerProductSpace.norm_rankOne, PiTensorProduct.mapLMultilinear_toFun_apply, ContinuousMultilinearMap.uncurryRight_norm, flipAlternating_apply_apply, IsSymmSndFDerivAt.eq, norm_iteratedFDerivWithin_le_of_bilinear_aux, fderiv_inv', Continuous.fderiv_one
uniformSpace 📖	CompOp	13 math math: isUniformEmbedding_restrictScalars, completeSpace, uniformContinuous_restrictScalars, isUniformAddGroup, uniformContinuousConstSMul, isUniformInducing_postcomp, instCompleteSpace, SeparatingDual.completeSpace_continuousLinearMap_iff, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology, isUniformEmbedding_postcomp, isUniformEmbedding_toUniformOnFun, UniformCauchySeqOnFilter.one_smulRight, DoubleCentralizer.isUniformEmbedding_toProdMulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_restrictScalarsL 📖	mathematical	—	toLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module restrictScalarsL restrictScalarsₗ LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsTopologicalAddGroup.toContinuousAdd
coe_restrict_scalarsL' 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module funLike restrictScalarsL restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsTopologicalAddGroup.toContinuousAdd
completeSpace 📖	mathematical	Topology.IsCoherentWith setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CompleteSpace ContinuousLinearMap UniformSpace.toTopologicalSpace uniformSpace	—	UniformConvergenceCLM.completeSpace Bornology.sUnion_isVonNBounded_eq_univ
continuousConstSMul 📖	mathematical	—	ContinuousConstSMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	UniformConvergenceCLM.instContinuousConstSMul
continuousSMul 📖	mathematical	—	ContinuousSMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass topologicalSpace	—	UniformConvergenceCLM.continuousSMul
continuous_restrictScalars 📖	mathematical	—	Continuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid topologicalSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	Topology.IsEmbedding.continuous LinearMap.IsScalarTower.compatibleSMul isEmbedding_restrictScalars
coprodEquivL_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule funLike ContinuousLinearEquiv RingHomInvPair.ids topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup Prod.instAddCommGroup module EquivLike.toFunLike ContinuousLinearEquiv.equivLike coprodEquivL AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd
coprodEquivL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instTopologicalSpaceProd Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid Prod.instModule topologicalSpace Prod.instAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm coprodEquivL comp inl inr	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd
eventually_nhds_zero_mapsTo 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Filter Filter.instMembership nhds	Filter.Eventually ContinuousLinearMap Set.MapsTo DFunLike.coe funLike topologicalSpace zero	—	UniformConvergenceCLM.eventually_nhds_zero_mapsTo
hasBasis_nhds_zero 📖	mathematical	—	Filter.HasBasis ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set nhds topologicalSpace zero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter Filter.instMembership setOf	—	hasBasis_nhds_zero_of_basis Filter.basis_sets
hasBasis_nhds_zero_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Set topologicalSpace zero Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction setOf	—	UniformConvergenceCLM.hasBasis_nhds_zero_of_basis Bornology.isVonNBounded_empty directedOn_of_sup_mem Bornology.IsVonNBounded.union
instCompleteSpace 📖	mathematical	—	CompleteSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace	—	completeSpace Topology.IsCoherentWith.of_seq Bornology.IsVonNBounded.insert Filter.Tendsto.isVonNBounded_range
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace	—	UniformConvergenceCLM.continuousEvalConst Bornology.sUnion_isVonNBounded_eq_univ
instT2Space 📖	mathematical	—	T2Space ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace	—	UniformConvergenceCLM.t2Space Bornology.sUnion_isVonNBounded_eq_univ
isEmbedding_postcomp 📖	mathematical	Topology.IsEmbedding DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	topologicalSpace comp	—	isInducing_postcomp Topology.IsEmbedding.isInducing cancel_left Topology.IsEmbedding.injective
isEmbedding_restrictScalars 📖	mathematical	—	Topology.IsEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid topologicalSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsUniformEmbedding.isEmbedding isUniformAddGroup_of_addCommGroup LinearMap.IsScalarTower.compatibleSMul isUniformEmbedding_restrictScalars
isInducing_postcomp 📖	mathematical	Topology.IsInducing DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	topologicalSpace comp	—	IsUniformInducing.isInducing isUniformAddGroup_of_addCommGroup isUniformInducing_postcomp AddMonoidHom.isUniformInducing_of_isInducing DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass
isUniformAddGroup 📖	mathematical	—	IsUniformAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace AddCommGroup.toAddGroup addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing IsUniformAddGroup.to_topologicalAddGroup	—	UniformConvergenceCLM.instIsUniformAddGroup
isUniformEmbedding_postcomp 📖	mathematical	IsUniformEmbedding DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid funLike	uniformSpace comp	—	UniformConvergenceCLM.isUniformEmbedding_postcomp
isUniformEmbedding_restrictScalars 📖	mathematical	—	IsUniformEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	LinearMap.IsScalarTower.compatibleSMul IsUniformEmbedding.of_comp_iff isUniformEmbedding_toUniformOnFun Bornology.IsVonNBounded.extend_scalars Bornology.IsVonNBounded.restrict_scalars
isUniformEmbedding_toUniformOnFun 📖	mathematical	—	IsUniformEmbedding ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace UniformOnFun setOf Set Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid uniformSpace UniformOnFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun funLike	—	UniformConvergenceCLM.isUniformEmbedding_coeFn
isUniformInducing_postcomp 📖	mathematical	IsUniformInducing DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid funLike	uniformSpace comp	—	UniformConvergenceCLM.isUniformInducing_postcomp
isVonNBounded_iff 📖	mathematical	—	Bornology.IsVonNBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing AddCommMonoid.toAddMonoid Module.toDistribMulAction zero topologicalSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image2 DFunLike.coe funLike	—	UniformConvergenceCLM.isVonNBounded_iff
isVonNBounded_image2_apply 📖	mathematical	Bornology.IsVonNBounded ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing AddCommMonoid.toAddMonoid zero topologicalSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Set.image2 DFunLike.coe funLike	—	UniformConvergenceCLM.isVonNBounded_image2_apply
map_add₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_add add_apply
map_neg₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass neg_apply
map_smul₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike RingHom.id Semiring.toNonAssocSemiring topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_smul smul_apply
map_smulₛₗ₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_smulₛₗ smul_apply
map_sub₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass sub_apply
map_zero₂ 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self map_zero zero_apply
nhds_zero_eq 📖	mathematical	—	nhds ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace zero iInf Filter Set Filter.instInfSet Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.instMembership Filter.principal setOf Set.MapsTo DFunLike.coe funLike	—	UniformConvergenceCLM.nhds_zero_eq
nhds_zero_eq_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace zero iInf Filter Set Filter.instInfSet Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Filter.principal setOf Set.MapsTo DFunLike.coe funLike	—	UniformConvergenceCLM.nhds_zero_eq_of_basis
postcompCompactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike postcompCompactConvergenceCLM comp	—	smulCommClass_self
postcompUniformConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformConvergenceCLM UniformConvergenceCLM.instTopologicalSpace AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike postcompUniformConvergenceCLM comp	—	smulCommClass_self
postcomp_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike postcomp comp	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
postcomp_uniformConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformConvergenceCLM UniformConvergenceCLM.instTopologicalSpace AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike postcompUniformConvergenceCLM comp	—	postcompUniformConvergenceCLM_apply
precompCompactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike precompCompactConvergenceCLM comp	—	smulCommClass_self
precompUniformConvergenceCLM_apply 📖	mathematical	Set.MapsTo Set Set.image DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	RingHom.id Semiring.toNonAssocSemiring UniformConvergenceCLM UniformConvergenceCLM.instTopologicalSpace UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing precompUniformConvergenceCLM comp	—	smulCommClass_self
precomp_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing funLike precomp comp	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
precomp_uniformConvergenceCLM_apply 📖	mathematical	Set.MapsTo Set Set.image DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	RingHom.id Semiring.toNonAssocSemiring UniformConvergenceCLM UniformConvergenceCLM.instTopologicalSpace UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing precompUniformConvergenceCLM comp	—	precompUniformConvergenceCLM_apply
prodL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instTopologicalSpaceProd topologicalSpace Prod.instAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup Prod.instModule Prod.instAddCommGroup Prod.instIsTopologicalAddGroup Prod.continuousAdd AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid module Prod.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction Module.toDistribMulAction Prod.continuousConstSMul EquivLike.toFunLike ContinuousLinearEquiv.equivLike prodL prod	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd Prod.instIsTopologicalAddGroup Prod.continuousAdd Prod.smulCommClass Prod.continuousConstSMul
toBilinForm_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module toBilinForm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace funLike topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing module Algebra.to_smulCommClass Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul
toBilinForm_inj 📖	mathematical	—	toBilinForm	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul toBilinForm_injective
toBilinForm_injective 📖	mathematical	—	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing LinearMap.BilinForm toBilinForm	—	toLinearMap₁₂_injective
toLinearMap₁₂_apply 📖	mathematical	—	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing toLinearMap₁₂ ContinuousLinearMap funLike topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
toLinearMap₁₂_inj 📖	mathematical	—	toLinearMap₁₂	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self toLinearMap₁₂_injective
toLinearMap₁₂_injective 📖	mathematical	—	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap LinearMap.addCommMonoid LinearMap.module toLinearMap₁₂	—	IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
toSpanSingletonCLE_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Semiring.toModule funLike ContinuousLinearEquiv RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace topologicalSpace SeminormedAddCommGroup.toAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousLinearEquiv.equivLike toSpanSingletonCLE	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul
toSpanSingletonCLE_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddCommGroup.toAddCommMonoid NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace topologicalSpace SeminormedAddCommGroup.toAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm toSpanSingletonCLE NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule funLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul
toUniformConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM UniformConvergenceCLM.instFunLike LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ContinuousLinearMap AddCommGroup.toAddCommMonoid addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup UniformConvergenceCLM.instAddCommGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing UniformConvergenceCLM.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toUniformConvergenceCLM funLike	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
toUniformConvergenceCLM_continuous 📖	mathematical	Set Set.instHasSubset setOf Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Continuous ContinuousLinearMap UniformConvergenceCLM topologicalSpace UniformConvergenceCLM.instTopologicalSpace DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids addCommMonoid IsTopologicalAddGroup.toContinuousAdd UniformConvergenceCLM.instAddCommGroup module smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing UniformConvergenceCLM.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toUniformConvergenceCLM	—	continuous_id_of_le UniformConvergenceCLM.topologicalSpace_mono
toUniformConvergenceCLM_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformConvergenceCLM UniformConvergenceCLM.instAddCommGroup addCommMonoid IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm toUniformConvergenceCLM UniformConvergenceCLM.instFunLike	—	RingHomInvPair.ids IsTopologicalAddGroup.toContinuousAdd smulCommClass_self
topologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid topologicalSpace AddCommGroup.toAddGroup addCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing	—	UniformConvergenceCLM.instIsTopologicalAddGroup
uniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass	—	UniformConvergenceCLM.instUniformContinuousConstSMul
uniformContinuous_restrictScalars 📖	mathematical	—	UniformContinuous ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace uniformSpace restrictScalars LinearMap.IsScalarTower.compatibleSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul Semifield.toCommSemiring Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NormedAlgebra.toAlgebra	—	IsUniformInducing.uniformContinuous LinearMap.IsScalarTower.compatibleSMul IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_restrictScalars

UniformConvergenceCLM

Definitions

Name	Category	Theorems
instAddCommGroup 📖	CompOp	86 math math: TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, ContinuousLinearMap.precompUniformConvergenceCLM_apply, CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, TemperedDistribution.lineDerivOp_fourier_eq, smul_apply, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, coe_zero, TemperedDistribution.smulLeftCLM_neg, PointwiseConvergenceCLM.postcomp_apply, TemperedDistribution.instLineDerivLeftSMulReal, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.instFourierAdd, PointwiseConvergenceCLM.instLocallyConvexSpace, TemperedDistribution.instFourierSMul, ContinuousLinearMap.toUniformConvergenceCLM_apply, continuousSMul, add_apply, PointwiseConvergenceCLM.isInducing_inducingFn, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, PointwiseConvergenceCLM.equivWeakDual_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, PointwiseConvergenceCLM.equivWeakDual_symm_apply, Distribution.mapCLM_apply, sub_apply, instIsUniformAddGroup, hasBasis_nhds_zero_of_basis, PointwiseConvergenceCLM.coeLMₛₗ_apply, ContinuousLinearMap.postcompCompactConvergenceCLM_apply, TemperedDistribution.instLineDerivSMulReal, PointwiseConvergenceCLM.coeLM_apply, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_eq_sum, CompactConvergenceCLM.hasBasis_nhds_zero, TemperedDistribution.smulLeftCLM_add, PointwiseConvergenceCLM.precomp_apply, precomp_compactConvergenceCLM_apply, hasBasis_nhds_zero, instIsTopologicalAddGroup, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instFourierInvAdd, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.instLineDerivAdd, TemperedDistribution.instLineDerivSMulComplex, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, ContinuousLinearMap.precompCompactConvergenceCLM_apply, instContinuousConstSMul, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, sum_apply, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, PointwiseConvergenceCLM.hasBasis_nhds_zero, TemperedDistribution.lineDerivOp_fourierInv_eq, CompactConvergenceCLM.continuousSMul, instUniformContinuousConstSMul, ContinuousLinearMap.toUniformConvergenceCLM_continuous, TemperedDistribution.smulLeftCLM_const, TemperedDistribution.smulLeftCLM_sum, eventually_nhds_zero_mapsTo, PointwiseConvergenceCLM.evalCLM_apply, SchwartzMap.coe_apply, TemperedDistribution.smulLeftCLM_smul, PointwiseConvergenceCLM.withSeminorms, TemperedDistribution.derivCLM_apply_apply, PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis, ContinuousLinearMap.precomp_uniformConvergenceCLM_apply, ContinuousLinearMap.postcompUniformConvergenceCLM_apply, ContinuousLinearMap.toPointwiseConvergenceCLM_apply, nhds_zero_eq, ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply, isVonNBounded_iff, locallyConvexSpace, postcomp_compactConvergenceCLM_apply, TemperedDistribution.laplacianCLM_apply, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply, nhds_zero_eq_of_basis, neg_apply
instDistribMulAction 📖	CompOp	17 math math: TemperedDistribution.lineDerivOp_fourier_eq, smul_apply, TemperedDistribution.instLineDerivLeftSMulReal, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.instFourierSMul, continuousSMul, TemperedDistribution.instLineDerivSMulReal, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instLineDerivSMulComplex, instContinuousConstSMul, TemperedDistribution.lineDerivOp_fourierInv_eq, CompactConvergenceCLM.continuousSMul, instUniformContinuousConstSMul, TemperedDistribution.smulLeftCLM_const, TemperedDistribution.smulLeftCLM_smul, isVonNBounded_iff
instFunLike 📖	CompOp	47 math math: isEmbedding_coeFn, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, smul_apply, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, coe_zero, PointwiseConvergenceCLM.tendsto_nhds, Function.HasTemperateGrowth.toTemperedDistribution_apply, ContinuousLinearMap.toUniformConvergenceCLM_apply, TemperedDistribution.delta_apply, SchwartzMap.delta_apply, PointwiseConvergenceCLM.isEmbedding_coeFn, add_apply, SchwartzMap.toTemperedDistributionCLM_apply_apply, topologicalSpace_eq, Distribution.mapCLM_apply, sub_apply, PointwiseConvergenceCLM.continuousEvalConst, MeasureTheory.Measure.toTemperedDistribution_apply, isVonNBounded_image2_apply, isUniformInducing_coeFn, TemperedDistribution.fourierTransform_apply, continuousEvalConst, CompactConvergenceCLM.instContinuousEvalConst, TemperedDistribution.fourierInv_apply, PointwiseConvergenceCLM.tendsto_nhds_atTop, PointwiseConvergenceCLM.tendsto_iff_forall_tendsto, sum_apply, tendsto_iff_tendstoUniformlyOn, uniformSpace_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.lineDerivOp_apply_apply, MeasureTheory.Lp.toTemperedDistribution_apply, eventually_nhds_zero_mapsTo, TemperedDistribution.fourier_apply, SchwartzMap.coe_apply, TemperedDistribution.derivCLM_apply_apply, instContinuousSemilinearMapClass, nhds_zero_eq, ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, TemperedDistribution.fourierTransformInv_apply, isUniformEmbedding_coeFn, PointwiseConvergenceCLM.isUniformEmbedding_coeFn, isVonNBounded_iff, ext_iff, TemperedDistribution.smulLeftCLM_apply_apply, nhds_zero_eq_of_basis, neg_apply
instModule 📖	CompOp	55 math math: TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, ContinuousLinearMap.precompUniformConvergenceCLM_apply, TemperedDistribution.lineDerivOp_fourier_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, TemperedDistribution.smulLeftCLM_neg, PointwiseConvergenceCLM.postcomp_apply, TemperedDistribution.fourierInv_lineDerivOp_eq, PointwiseConvergenceCLM.instLocallyConvexSpace, ContinuousLinearMap.toUniformConvergenceCLM_apply, PointwiseConvergenceCLM.isInducing_inducingFn, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, PointwiseConvergenceCLM.equivWeakDual_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, PointwiseConvergenceCLM.equivWeakDual_symm_apply, Distribution.mapCLM_apply, PointwiseConvergenceCLM.coeLMₛₗ_apply, ContinuousLinearMap.postcompCompactConvergenceCLM_apply, PointwiseConvergenceCLM.coeLM_apply, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.smulLeftCLM_add, PointwiseConvergenceCLM.precomp_apply, precomp_compactConvergenceCLM_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, ContinuousLinearMap.precompCompactConvergenceCLM_apply, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, TemperedDistribution.lineDerivOp_fourierInv_eq, ContinuousLinearMap.toUniformConvergenceCLM_continuous, TemperedDistribution.smulLeftCLM_const, TemperedDistribution.smulLeftCLM_sum, PointwiseConvergenceCLM.evalCLM_apply, SchwartzMap.coe_apply, TemperedDistribution.smulLeftCLM_smul, PointwiseConvergenceCLM.withSeminorms, TemperedDistribution.derivCLM_apply_apply, ContinuousLinearMap.precomp_uniformConvergenceCLM_apply, ContinuousLinearMap.postcompUniformConvergenceCLM_apply, ContinuousLinearMap.toPointwiseConvergenceCLM_apply, ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply, locallyConvexSpace, postcomp_compactConvergenceCLM_apply, TemperedDistribution.laplacianCLM_apply, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply
instTopologicalSpace 📖	CompOp	84 math math: isEmbedding_coeFn, TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, ContinuousLinearMap.precompUniformConvergenceCLM_apply, CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, TemperedDistribution.lineDerivOp_fourier_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, PointwiseConvergenceCLM.continuous_of_continuous_eval, PointwiseConvergenceCLM.tendsto_nhds, topologicalSpace_mono, TemperedDistribution.smulLeftCLM_neg, PointwiseConvergenceCLM.postcomp_apply, TemperedDistribution.fourierInv_lineDerivOp_eq, PointwiseConvergenceCLM.instLocallyConvexSpace, TemperedDistribution.instContinuousFourier, PointwiseConvergenceCLM.instT2Space, continuousSMul, PointwiseConvergenceCLM.isEmbedding_coeFn, PointwiseConvergenceCLM.isInducing_inducingFn, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, PointwiseConvergenceCLM.equivWeakDual_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, SchwartzMap.toTemperedDistributionCLM_apply_apply, TemperedDistribution.smulLeftCLM_sub, PointwiseConvergenceCLM.equivWeakDual_symm_apply, uniformity_toTopologicalSpace_eq, topologicalSpace_eq, Distribution.mapCLM_apply, t2Space, hasBasis_nhds_zero_of_basis, ContinuousLinearMap.postcompCompactConvergenceCLM_apply, PointwiseConvergenceCLM.continuousEvalConst, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.instContinuousLineDeriv, CompactConvergenceCLM.hasBasis_nhds_zero, TemperedDistribution.smulLeftCLM_add, PointwiseConvergenceCLM.precomp_apply, continuousEvalConst, precomp_compactConvergenceCLM_apply, hasBasis_nhds_zero, instIsTopologicalAddGroup, CompactConvergenceCLM.instContinuousEvalConst, PointwiseConvergenceCLM.tendsto_nhds_atTop, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, CompactConvergenceCLM.instT2Space, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, ContinuousLinearMap.precompCompactConvergenceCLM_apply, PointwiseConvergenceCLM.tendsto_iff_forall_tendsto, instContinuousConstSMul, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, tendsto_iff_tendstoUniformlyOn, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, PointwiseConvergenceCLM.hasBasis_nhds_zero, TemperedDistribution.lineDerivOp_fourierInv_eq, CompactConvergenceCLM.continuousSMul, ContinuousLinearMap.toUniformConvergenceCLM_continuous, TemperedDistribution.smulLeftCLM_const, TemperedDistribution.smulLeftCLM_sum, eventually_nhds_zero_mapsTo, TemperedDistribution.instContinuousFourierInv, PointwiseConvergenceCLM.evalCLM_apply, SchwartzMap.coe_apply, TemperedDistribution.smulLeftCLM_smul, PointwiseConvergenceCLM.withSeminorms, TemperedDistribution.derivCLM_apply_apply, PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis, ContinuousLinearMap.precomp_uniformConvergenceCLM_apply, ContinuousLinearMap.postcompUniformConvergenceCLM_apply, ContinuousLinearMap.toPointwiseConvergenceCLM_apply, nhds_zero_eq, ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply, isVonNBounded_iff, locallyConvexSpace, postcomp_compactConvergenceCLM_apply, TemperedDistribution.laplacianCLM_apply, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply, nhds_zero_eq_of_basis
instUniformSpace 📖	CompOp	11 math math: uniformSpace_mono, uniformity_toTopologicalSpace_eq, instIsUniformAddGroup, completeSpace, isUniformEmbedding_postcomp, isUniformInducing_coeFn, uniformSpace_eq, instUniformContinuousConstSMul, isUniformEmbedding_coeFn, PointwiseConvergenceCLM.isUniformEmbedding_coeFn, isUniformInducing_postcomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroup	—	—
coe_zero 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Pi.instZero	—	—
completeSpace 📖	mathematical	Topology.IsCoherentWith Set.sUnion Set.univ	CompleteSpace UniformConvergenceCLM UniformSpace.toTopologicalSpace instUniformSpace	—	completeSpace_iff_isComplete_range isUniformInducing_coeFn IsClosed.isComplete UniformOnFun.instCompleteSpace UniformOnFun.isClosed_setOf_continuous ContinuousLinearMap.range_coeFn_eq IsClosed.inter IsClosed.preimage UniformContinuous.continuous UniformOnFun.uniformContinuous_toFun LinearMap.isClosed_range_coe ContinuousSMul.continuousConstSMul IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup SeparationQuotient.instIsUniformAddGroup IsUniformInducing.completeSpace_congr RingHomCompTriple.right_ids isUniformInducing_postcomp SeparationQuotient.postcomp_mkCLM_surjective SeparationQuotient.instContinuousSMul SeparationQuotient.instCompleteSpace SeparationQuotient.t2Space instR1Space UniformSpace.to_regularSpace
continuousEvalConst 📖	mathematical	Set.sUnion Set.univ	ContinuousEvalConst UniformConvergenceCLM instFunLike instTopologicalSpace	—	Continuous.comp UniformContinuous.continuous UniformOnFun.uniformContinuous_eval Topology.IsEmbedding.continuous IsUniformAddGroup.to_topologicalAddGroup isUniformAddGroup_of_addCommGroup isEmbedding_coeFn
continuousSMul 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	ContinuousSMul UniformConvergenceCLM instAddCommGroup instDistribMulAction smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace instTopologicalSpace	—	smulCommClass_self ContinuousSMul.continuousConstSMul UniformOnFun.continuousSMul_induced_of_image_bounded isUniformAddGroup_of_addCommGroup LinearMap.semilinearMapClass Bornology.IsVonNBounded.image
eventually_nhds_zero_mapsTo 📖	mathematical	Set Set.instMembership Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Filter.Eventually UniformConvergenceCLM Set.MapsTo DFunLike.coe instFunLike instTopologicalSpace instAddCommGroup	—	nhds_zero_eq Filter.mem_iInf_of_mem Filter.mem_principal_self
ext 📖	—	DFunLike.coe UniformConvergenceCLM instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike	—	ext
hasBasis_nhds_zero 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset	Filter.HasBasis UniformConvergenceCLM nhds instTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup Set.instMembership Filter Filter.instMembership setOf	—	hasBasis_nhds_zero_of_basis Filter.basis_sets
hasBasis_nhds_zero_of_basis 📖	mathematical	Set.Nonempty Set DirectedOn Set.instHasSubset Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	UniformConvergenceCLM instTopologicalSpace instAddCommGroup Set.instMembership setOf	—	IsUniformAddGroup.to_topologicalAddGroup isUniformAddGroup_of_addCommGroup Topology.IsInducing.nhds_eq_comap Topology.IsEmbedding.isInducing isEmbedding_coeFn Filter.HasBasis.comap UniformOnFun.hasBasis_nhds_zero_of_basis
instContinuousConstSMul 📖	mathematical	—	ContinuousConstSMul UniformConvergenceCLM instTopologicalSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instDistribMulAction	—	isUniformAddGroup_of_addCommGroup uniformContinuousConstSMul_of_continuousConstSMul UniformContinuousConstSMul.to_continuousConstSMul instUniformContinuousConstSMul
instContinuousSemilinearMapClass 📖	mathematical	—	ContinuousSemilinearMapClass UniformConvergenceCLM DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instFunLike	—	ContinuousLinearMap.continuousSemilinearMapClass
instIsTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup UniformConvergenceCLM instTopologicalSpace AddCommGroup.toAddGroup instAddCommGroup	—	IsUniformAddGroup.to_topologicalAddGroup isUniformAddGroup_of_addCommGroup instIsUniformAddGroup
instIsUniformAddGroup 📖	mathematical	—	IsUniformAddGroup UniformConvergenceCLM UniformSpace.toTopologicalSpace instUniformSpace AddCommGroup.toAddGroup instAddCommGroup IsUniformAddGroup.to_topologicalAddGroup	—	IsUniformAddGroup.to_topologicalAddGroup IsUniformInducing.isUniformAddGroup instIsUniformAddGroupUniformOnFun AddMonoidHom.instAddMonoidHomClass IsUniformEmbedding.toIsUniformInducing isUniformEmbedding_coeFn
instUniformContinuousConstSMul 📖	mathematical	—	UniformContinuousConstSMul UniformConvergenceCLM UniformSpace.toTopologicalSpace instUniformSpace SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup IsUniformAddGroup.to_topologicalAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instDistribMulAction UniformContinuousConstSMul.to_continuousConstSMul	—	IsUniformInducing.uniformContinuousConstSMul IsUniformAddGroup.to_topologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul UniformFunOn.uniformContinuousConstSMul isUniformInducing_coeFn
isEmbedding_coeFn 📖	mathematical	—	Topology.IsEmbedding UniformConvergenceCLM UniformSpace.toTopologicalSpace UniformOnFun instTopologicalSpace IsUniformAddGroup.to_topologicalAddGroup AddCommGroup.toAddGroup UniformOnFun.topologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun instFunLike	—	IsUniformEmbedding.isEmbedding isUniformEmbedding_coeFn
isUniformEmbedding_coeFn 📖	mathematical	—	IsUniformEmbedding UniformConvergenceCLM UniformSpace.toTopologicalSpace UniformOnFun instUniformSpace UniformOnFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun instFunLike	—	isUniformInducing_coeFn DFunLike.coe_injective
isUniformEmbedding_postcomp 📖	mathematical	IsUniformEmbedding DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	UniformConvergenceCLM instUniformSpace ContinuousLinearMap.comp	—	isUniformInducing_postcomp IsUniformEmbedding.isUniformInducing ContinuousLinearMap.cancel_left IsUniformEmbedding.injective
isUniformInducing_coeFn 📖	mathematical	—	IsUniformInducing UniformConvergenceCLM UniformSpace.toTopologicalSpace UniformOnFun instUniformSpace UniformOnFun.uniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun instFunLike	—	—
isUniformInducing_postcomp 📖	mathematical	IsUniformInducing DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike	UniformConvergenceCLM instUniformSpace ContinuousLinearMap.comp	—	IsUniformInducing.of_comp_iff isUniformInducing_coeFn IsUniformInducing.comp UniformOnFun.postcomp_isUniformInducing
isVonNBounded_iff 📖	mathematical	—	Bornology.IsVonNBounded UniformConvergenceCLM NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing instDistribMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instTopologicalSpace Set.image2 DFunLike.coe instFunLike	—	isVonNBounded_image2_apply nhds_zero_eq Filter.mem_absorbing Absorbs.eq_1 Filter.mp_mem Bornology.eventually_ne_cobounded Filter.univ_mem' Set.mem_smul_set_iff_inv_smul_mem₀ Set.mem_image2_of_mem
isVonNBounded_image2_apply 📖	mathematical	Bornology.IsVonNBounded UniformConvergenceCLM SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing instDistribMulAction NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instTopologicalSpace Set Set.instMembership	Set.image2 DFunLike.coe instFunLike	—	Filter.mp_mem eventually_nhds_zero_mapsTo Filter.univ_mem' Set.image2_subset_iff Set.smul_mem_smul_set
neg_apply 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup	—	—
nhds_zero_eq 📖	mathematical	—	nhds UniformConvergenceCLM instTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroup iInf Filter Set Filter.instInfSet Set.instMembership Filter.instMembership Filter.principal setOf Set.MapsTo DFunLike.coe instFunLike	—	nhds_zero_eq_of_basis Filter.basis_sets
nhds_zero_eq_of_basis 📖	mathematical	Filter.HasBasis nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	UniformConvergenceCLM instTopologicalSpace instAddCommGroup iInf Filter Set Filter.instInfSet Set.instMembership Filter.principal setOf Set.MapsTo DFunLike.coe instFunLike	—	IsUniformAddGroup.to_topologicalAddGroup isUniformAddGroup_of_addCommGroup Topology.IsInducing.nhds_eq_comap Topology.IsEmbedding.isInducing isEmbedding_coeFn UniformOnFun.nhds_eq_of_basis Filter.HasBasis.uniformity_of_nhds_zero iInf_congr_Prop sub_zero Filter.comap_iInf Filter.comap_principal
smul_apply 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instDistribMulAction	—	—
sub_apply 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup	—	—
sum_apply 📖	mathematical	—	DFunLike.coe UniformConvergenceCLM instFunLike Finset.sum AddCommGroup.toAddCommMonoid instAddCommGroup	—	ContinuousLinearMap.sum_apply IsTopologicalAddGroup.toContinuousAdd
t2Space 📖	mathematical	Set.sUnion Set.univ	T2Space UniformConvergenceCLM instTopologicalSpace	—	Topology.IsEmbedding.t2Space IsUniformAddGroup.to_topologicalAddGroup isUniformAddGroup_of_addCommGroup UniformOnFun.t2Space_of_covering isEmbedding_coeFn
tendsto_iff_tendstoUniformlyOn 📖	mathematical	—	Filter.Tendsto UniformConvergenceCLM UniformSpace.toTopologicalSpace nhds instTopologicalSpace IsUniformAddGroup.to_topologicalAddGroup AddCommGroup.toAddGroup TendstoUniformlyOn DFunLike.coe instFunLike	—	IsUniformAddGroup.to_topologicalAddGroup Topology.IsEmbedding.tendsto_nhds_iff isEmbedding_coeFn UniformOnFun.tendsto_iff_tendstoUniformlyOn
topologicalSpace_eq 📖	mathematical	—	instTopologicalSpace UniformSpace.toTopologicalSpace IsUniformAddGroup.to_topologicalAddGroup AddCommGroup.toAddGroup TopologicalSpace.induced UniformConvergenceCLM UniformOnFun DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun instFunLike UniformOnFun.topologicalSpace	—	IsUniformAddGroup.to_topologicalAddGroup instTopologicalSpace.eq_1 IsUniformAddGroup.rightUniformSpace_eq
topologicalSpace_mono 📖	mathematical	Set Set.instHasSubset	TopologicalSpace UniformConvergenceCLM Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder instTopologicalSpace	—	UniformSpace.toTopologicalSpace_mono isUniformAddGroup_of_addCommGroup uniformSpace_mono
uniformSpace_eq 📖	mathematical	—	instUniformSpace UniformSpace.comap UniformConvergenceCLM UniformSpace.toTopologicalSpace UniformOnFun DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike UniformOnFun.ofFun instFunLike UniformOnFun.uniformSpace	—	instUniformSpace.eq_1 UniformSpace.replaceTopology_eq
uniformSpace_mono 📖	mathematical	Set Set.instHasSubset	UniformSpace UniformConvergenceCLM UniformSpace.toTopologicalSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace instUniformSpace	—	uniformSpace_eq UniformSpace.comap_mono UniformOnFun.mono le_refl
uniformity_toTopologicalSpace_eq 📖	mathematical	—	UniformSpace.toTopologicalSpace UniformConvergenceCLM instUniformSpace instTopologicalSpace IsUniformAddGroup.to_topologicalAddGroup AddCommGroup.toAddGroup	—	—

(root)

Definitions

Name	Category	Theorems
CompactConvergenceCLM 📖	CompOp	11 math math: ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, ContinuousLinearMap.postcompCompactConvergenceCLM_apply, CompactConvergenceCLM.hasBasis_nhds_zero, precomp_compactConvergenceCLM_apply, CompactConvergenceCLM.instContinuousEvalConst, CompactConvergenceCLM.instT2Space, ContinuousLinearMap.precompCompactConvergenceCLM_apply, CompactConvergenceCLM.continuousSMul, postcomp_compactConvergenceCLM_apply
UniformConvergenceCLM 📖	CompOp	42 math math: UniformConvergenceCLM.isEmbedding_coeFn, ContinuousLinearMap.precompUniformConvergenceCLM_apply, UniformConvergenceCLM.smul_apply, UniformConvergenceCLM.coe_zero, UniformConvergenceCLM.topologicalSpace_mono, ContinuousLinearMap.toUniformConvergenceCLM_apply, UniformConvergenceCLM.continuousSMul, UniformConvergenceCLM.add_apply, UniformConvergenceCLM.uniformSpace_mono, UniformConvergenceCLM.uniformity_toTopologicalSpace_eq, UniformConvergenceCLM.topologicalSpace_eq, UniformConvergenceCLM.sub_apply, UniformConvergenceCLM.t2Space, UniformConvergenceCLM.instIsUniformAddGroup, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, UniformConvergenceCLM.completeSpace, UniformConvergenceCLM.isUniformEmbedding_postcomp, UniformConvergenceCLM.isUniformInducing_coeFn, UniformConvergenceCLM.continuousEvalConst, UniformConvergenceCLM.hasBasis_nhds_zero, UniformConvergenceCLM.instIsTopologicalAddGroup, UniformConvergenceCLM.instContinuousConstSMul, UniformConvergenceCLM.sum_apply, UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn, UniformConvergenceCLM.uniformSpace_eq, UniformConvergenceCLM.instUniformContinuousConstSMul, ContinuousLinearMap.toUniformConvergenceCLM_continuous, UniformConvergenceCLM.eventually_nhds_zero_mapsTo, TemperedDistribution.smulLeftCLM_smul, ContinuousLinearMap.precomp_uniformConvergenceCLM_apply, ContinuousLinearMap.postcompUniformConvergenceCLM_apply, UniformConvergenceCLM.instContinuousSemilinearMapClass, UniformConvergenceCLM.nhds_zero_eq, ContinuousLinearMap.toUniformConvergenceCLM_symm_apply, UniformConvergenceCLM.isUniformEmbedding_coeFn, ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply, UniformConvergenceCLM.isVonNBounded_iff, UniformConvergenceCLM.isUniformInducing_postcomp, UniformConvergenceCLM.locallyConvexSpace, UniformConvergenceCLM.ext_iff, UniformConvergenceCLM.nhds_zero_eq_of_basis, UniformConvergenceCLM.neg_apply
postcomp_compactConvergenceCLM 📖	CompOp	—
precomp_compactConvergenceCLM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
postcomp_compactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike ContinuousLinearMap.postcompCompactConvergenceCLM ContinuousLinearMap.comp	—	ContinuousLinearMap.postcompCompactConvergenceCLM_apply
precomp_compactConvergenceCLM_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring CompactConvergenceCLM UniformConvergenceCLM.instTopologicalSpace setOf Set IsCompact AddCommGroup.toAddCommMonoid UniformConvergenceCLM.instAddCommGroup UniformConvergenceCLM.instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing ContinuousLinearMap.funLike ContinuousLinearMap.precompCompactConvergenceCLM ContinuousLinearMap.comp	—	ContinuousLinearMap.precompCompactConvergenceCLM_apply

---

← Back to Index