UniformConvergenceCLM

📁 Source: Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean

Statistics

Metric	Count
Definitions postcompUniformConvergenceCLM, postcomp_uniformConvergenceCLM, precompUniformConvergenceCLM, precomp_uniformConvergenceCLM, toUniformConvergenceCLM, UniformConvergenceCLM, instAddCommGroup, instDistribMulAction, instFunLike, instModule, instTopologicalSpace, instUniformSpace	12
Theorems postcompUniformConvergenceCLM_apply, postcomp_uniformConvergenceCLM_apply, precompUniformConvergenceCLM_apply, precomp_uniformConvergenceCLM_apply, toUniformConvergenceCLM_apply, toUniformConvergenceCLM_symm_apply, add_apply, coe_zero, completeSpace, continuousEvalConst, continuousSMul, continuous_of_continuous_uncurry, 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	42
Total	54

ContinuousLinearMap

Definitions

Name	Category	Theorems
postcompUniformConvergenceCLM 📖	CompOp	2 math math: postcompUniformConvergenceCLM_apply, postcomp_uniformConvergenceCLM_apply
postcomp_uniformConvergenceCLM 📖	CompOp	—
precompUniformConvergenceCLM 📖	CompOp	2 math math: precompUniformConvergenceCLM_apply, precomp_uniformConvergenceCLM_apply
precomp_uniformConvergenceCLM 📖	CompOp	—
toUniformConvergenceCLM 📖	CompOp	3 math math: toUniformConvergenceCLM_apply, toUniformConvergenceCLM_continuous, toUniformConvergenceCLM_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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_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
precompUniformConvergenceCLM_apply 📖	mathematical	Set.MapsTo Set Set.image DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid funLike	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring 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 precompUniformConvergenceCLM comp	—	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	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring 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 precompUniformConvergenceCLM comp	—	precompUniformConvergenceCLM_apply
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_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

UniformConvergenceCLM

Definitions

Name	Category	Theorems
instAddCommGroup 📖	CompOp	100 math math: TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, continuous_of_continuous_uncurry, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, ContinuousLinearMap.precompUniformConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_smul, CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, TemperedDistribution.lineDerivOp_fourier_eq, smul_apply, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, Distribution.IsVanishingOn.smulLeftCLM, coe_zero, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, TemperedDistribution.smulLeftCLM_neg, PointwiseConvergenceCLM.postcomp_apply, TemperedDistribution.instLineDerivLeftSMulReal, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.instFourierAdd, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, PointwiseConvergenceCLM.instLocallyConvexSpace, TemperedDistribution.instFourierSMul, ContinuousLinearMap.toUniformConvergenceCLM_apply, Distribution.delta_eq_zero_of_notMem, continuousSMul, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, add_apply, PointwiseConvergenceCLM.isInducing_inducingFn, TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, TemperedDistribution.fourierMultiplierCLM_const, 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.fourierMultiplierCLM_toTemperedDistributionCLM_eq, TemperedDistribution.instLineDerivSMulReal, PointwiseConvergenceCLM.coeLM_apply, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_eq_sum, Distribution.dsupport_smulLeftCLM_subset, CompactConvergenceCLM.hasBasis_nhds_zero, TemperedDistribution.smulLeftCLM_add, PointwiseConvergenceCLM.precomp_apply, precomp_compactConvergenceCLM_apply, hasBasis_nhds_zero, instIsTopologicalAddGroup, TemperedDistribution.fourierMultiplierCLM_apply_apply, TemperedDistribution.instFourierInvSMul, TemperedDistribution.instFourierInvAdd, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.instLineDerivAdd, TemperedDistribution.instLineDerivSMulComplex, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, ContinuousLinearMap.precompCompactConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_sum, 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, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, 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	20 math math: TemperedDistribution.fourierMultiplierCLM_smul, TemperedDistribution.lineDerivOp_fourier_eq, smul_apply, TemperedDistribution.instLineDerivLeftSMulReal, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.instFourierSMul, continuousSMul, TemperedDistribution.fourierMultiplierCLM_const, 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, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM
instFunLike 📖	CompOp	57 math math: isEmbedding_coeFn, Distribution.delta_apply, Distribution.dsupport_delta, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, smul_apply, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, Distribution.IsVanishingOn.smulLeftCLM, 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, Distribution.IsVanishingOn.iteratedLineDerivOp, isVonNBounded_image2_apply, Distribution.dsupport_smulLeftCLM_subset, isUniformInducing_coeFn, TemperedDistribution.fourierTransform_apply, continuousEvalConst, TemperedDistribution.fourierMultiplierCLM_apply_apply, CompactConvergenceCLM.instContinuousEvalConst, Distribution.dsupport_iteratedLineDerivOp_subset, TemperedDistribution.fourierInv_apply, PointwiseConvergenceCLM.tendsto_nhds_atTop, Distribution.dsupport_lineDerivOp_subset, PointwiseConvergenceCLM.tendsto_iff_forall_tendsto, sum_apply, tendsto_iff_tendstoUniformlyOn, uniformSpace_eq, TemperedDistribution.laplacian_apply_apply, TemperedDistribution.isVanishingOn_delta, 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, Distribution.IsVanishingOn.lineDerivOp, ext_iff, TemperedDistribution.smulLeftCLM_apply_apply, nhds_zero_eq_of_basis, neg_apply
instModule 📖	CompOp	68 math math: TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, continuous_of_continuous_uncurry, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, ContinuousLinearMap.precompUniformConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_smul, TemperedDistribution.lineDerivOp_fourier_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, Distribution.IsVanishingOn.smulLeftCLM, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, TemperedDistribution.smulLeftCLM_neg, PointwiseConvergenceCLM.postcomp_apply, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, PointwiseConvergenceCLM.instLocallyConvexSpace, ContinuousLinearMap.toUniformConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, PointwiseConvergenceCLM.isInducing_inducingFn, TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, TemperedDistribution.fourierMultiplierCLM_const, 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, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, PointwiseConvergenceCLM.coeLM_apply, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, Distribution.dsupport_smulLeftCLM_subset, TemperedDistribution.smulLeftCLM_add, PointwiseConvergenceCLM.precomp_apply, precomp_compactConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_apply_apply, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, ContinuousLinearMap.precompCompactConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_sum, 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, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, locallyConvexSpace, postcomp_compactConvergenceCLM_apply, TemperedDistribution.laplacianCLM_apply, MeasureTheory.Lp.toTemperedDistribution_smul_eq, TemperedDistribution.smulLeftCLM_apply_apply
instTopologicalSpace 📖	CompOp	97 math math: isEmbedding_coeFn, TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, continuous_of_continuous_uncurry, ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply, ContinuousLinearMap.precompUniformConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_smul, CompactConvergenceCLM.hasBasis_nhds_zero_of_basis, TemperedDistribution.lineDerivOp_fourier_eq, ContinuousLinearEquiv.toCompactConvergenceCLM_apply, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, PointwiseConvergenceCLM.continuous_of_continuous_eval, Distribution.IsVanishingOn.smulLeftCLM, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, PointwiseConvergenceCLM.tendsto_nhds, topologicalSpace_mono, TemperedDistribution.smulLeftCLM_neg, PointwiseConvergenceCLM.postcomp_apply, TemperedDistribution.fourierInv_lineDerivOp_eq, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, PointwiseConvergenceCLM.instLocallyConvexSpace, TemperedDistribution.instContinuousFourier, PointwiseConvergenceCLM.instT2Space, continuousSMul, PointwiseConvergenceCLM.isEmbedding_coeFn, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, PointwiseConvergenceCLM.isInducing_inducingFn, TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, TemperedDistribution.fourierMultiplierCLM_const, 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, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, PointwiseConvergenceCLM.continuousEvalConst, TemperedDistribution.fourier_lineDerivOp_eq, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, TemperedDistribution.instContinuousLineDeriv, Distribution.dsupport_smulLeftCLM_subset, CompactConvergenceCLM.hasBasis_nhds_zero, TemperedDistribution.smulLeftCLM_add, PointwiseConvergenceCLM.precomp_apply, continuousEvalConst, precomp_compactConvergenceCLM_apply, hasBasis_nhds_zero, instIsTopologicalAddGroup, TemperedDistribution.fourierMultiplierCLM_apply_apply, CompactConvergenceCLM.instContinuousEvalConst, PointwiseConvergenceCLM.tendsto_nhds_atTop, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, CompactConvergenceCLM.instT2Space, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, ContinuousLinearMap.precompCompactConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_sum, 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, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, 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 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 Semifield.toDivisionSemiring Field.toSemifield NormedField.toField instDistribMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing ContinuousSMul.continuousConstSMul UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instTopologicalSpace	—	smulCommClass_self ContinuousSMul.continuousConstSMul UniformOnFun.continuousSMul_induced_of_image_bounded isUniformAddGroup_of_addCommGroup LinearMap.semilinearMapClass Bornology.IsVonNBounded.image
continuous_of_continuous_uncurry 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField 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 instTopologicalSpaceProd DFunLike.coe UniformConvergenceCLM instFunLike LinearMap instAddCommGroup instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing LinearMap.instFunLike	Continuous UniformConvergenceCLM NontriviallyNormedField.toNormedField instTopologicalSpace DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid instAddCommGroup instModule smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instFunLike	—	smulCommClass_self continuous_of_tendsto_nhds_zero IsTopologicalAddGroup.toContinuousAdd instIsTopologicalAddGroup DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass mem_nhds_prod_iff Continuous.tendsto' map_zero AddMonoidHomClass.toZeroHomClass Filter.Eventually.exists NormedField.nhdsNE_neBot Filter.Eventually.and Absorbs.eventually_nhdsNE_zero eventually_mem_nhdsWithin RingHom.surjective map_ne_zero IsSimpleRing.instNontrivial DivisionRing.isSimpleRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Filter.mp_mem set_smul_mem_nhds_zero_iff Filter.univ_mem' MulActionSemiHomClass.map_smulₛₗ SemilinearMapClass.toMulActionSemiHomClass smul_apply ContinuousSemilinearMapClass.toSemilinearMapClass instContinuousSemilinearMapClass nhds_zero_eq iInf_congr_Prop
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 nhds instTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid 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 Set 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	Filter.HasBasis UniformConvergenceCLM Set nhds instTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid 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	—	—
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	IsUniformEmbedding UniformConvergenceCLM UniformSpace.toTopologicalSpace instUniformSpace ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid	—	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	IsUniformInducing UniformConvergenceCLM UniformSpace.toTopologicalSpace instUniformSpace ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid	—	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	Bornology.IsVonNBounded SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image2 UniformConvergenceCLM 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	nhds UniformConvergenceCLM instTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid 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
UniformConvergenceCLM 📖	CompOp	46 math math: UniformConvergenceCLM.isEmbedding_coeFn, UniformConvergenceCLM.continuous_of_continuous_uncurry, ContinuousLinearMap.precompUniformConvergenceCLM_apply, TemperedDistribution.fourierMultiplierCLM_smul, UniformConvergenceCLM.smul_apply, UniformConvergenceCLM.coe_zero, UniformConvergenceCLM.topologicalSpace_mono, ContinuousLinearMap.toUniformConvergenceCLM_apply, UniformConvergenceCLM.continuousSMul, UniformConvergenceCLM.add_apply, TemperedDistribution.fourierMultiplierCLM_const, UniformConvergenceCLM.uniformSpace_mono, UniformConvergenceCLM.uniformity_toTopologicalSpace_eq, UniformConvergenceCLM.topologicalSpace_eq, UniformConvergenceCLM.sub_apply, UniformConvergenceCLM.t2Space, UniformConvergenceCLM.instIsUniformAddGroup, UniformConvergenceCLM.hasBasis_nhds_zero_of_basis, UniformConvergenceCLM.isVonNBounded_image2_apply, 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

---

← Back to Index