Documentation Verification Report

PointwiseConvergence

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

Statistics

Metric	Count
Definitions `toPointwiseConvergenceCLM`, `PointwiseConvergenceCLM`, `coeLM`, `coeLMₛₗ`, `equivWeakDual`, `evalCLM`, `postcomp`, `precomp`, `«term_→Lₚₜ[_]_»`, `«term_→SLₚₜ[_]_»`	10
Theorems `toPointwiseConvergenceCLM_apply`, `coeLM_apply`, `coeLMₛₗ_apply`, `continuousEvalConst`, `continuous_of_continuous_eval`, `equivWeakDual_apply`, `equivWeakDual_symm_apply`, `evalCLM_apply`, `hasBasis_nhds_zero`, `hasBasis_nhds_zero_of_basis`, `instT2Space`, `isEmbedding_coeFn`, `isUniformEmbedding_coeFn`, `postcomp_apply`, `precomp_apply`, `tendsto_iff_forall_tendsto`	16
Total	26

ContinuousLinearMap

Definitions

Name	Category	Theorems
`toPointwiseConvergenceCLM` 📖	CompOp	1 math math: `toPointwiseConvergenceCLM_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPointwiseConvergenceCLM_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` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem` `UniformConvergenceCLM.instAddCommGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformConvergenceCLM.instModule` `funLike` `toPointwiseConvergenceCLM`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self`

PointwiseConvergenceCLM

Definitions

Name	Category	Theorems
`coeLM` 📖	CompOp	1 math math: `coeLM_apply`
`coeLMₛₗ` 📖	CompOp	1 math math: `coeLMₛₗ_apply`
`equivWeakDual` 📖	CompOp	2 math math: `equivWeakDual_apply`, `equivWeakDual_symm_apply`
`evalCLM` 📖	CompOp	1 math math: `evalCLM_apply`
`postcomp` 📖	CompOp	1 math math: `postcomp_apply`
`precomp` 📖	CompOp	2 math math: `TemperedDistribution.lineDerivOpCLM_eq`, `precomp_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeLM_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `PointwiseConvergenceCLM` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `setOf` `Set` `Finite` `Set.Elem` `LinearMap.addCommMonoid` `UniformConvergenceCLM.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.module` `LinearMap.instFunLike` `coeLM` `ContinuousLinearMap.toLinearMap`	—	`smulCommClass_self`
`coeLMₛₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `PointwiseConvergenceCLM` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `setOf` `Set` `Finite` `Set.Elem` `LinearMap.addCommMonoid` `UniformConvergenceCLM.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `LinearMap.module` `LinearMap.instFunLike` `coeLMₛₗ` `ContinuousLinearMap.toLinearMap`	—	`smulCommClass_self`
`continuousEvalConst` 📖	mathematical	—	`ContinuousEvalConst` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instFunLike` `setOf` `Set` `Finite` `Set.Elem` `UniformConvergenceCLM.instTopologicalSpace`	—	`UniformConvergenceCLM.continuousEvalConst` `Set.sUnion_finite_eq_univ`
`continuous_of_continuous_eval` 📖	mathematical	`Continuous` `DFunLike.coe` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instFunLike` `setOf` `Set` `Finite` `Set.Elem`	`Continuous` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem`	—	`Topology.IsEmbedding.continuous_iff` `isEmbedding_coeFn`
`equivWeakDual_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PointwiseConvergenceCLM` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Set` `Finite` `Set.Elem` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `WeakDual` `Semifield.toCommSemiring` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `instTopologicalSpaceWeakDual` `instAddCommMonoidWeakDual` `UniformConvergenceCLM.instModule` `Algebra.to_smulCommClass` `Algebra.id` `WeakDual.instModule'` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equivWeakDual`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Algebra.to_smulCommClass`
`equivWeakDual_symm_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WeakDual` `Semifield.toCommSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceWeakDual` `instAddCommMonoidWeakDual` `PointwiseConvergenceCLM` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Set` `Finite` `Set.Elem` `UniformConvergenceCLM.instAddCommGroup` `WeakDual.instModule'` `Algebra.to_smulCommClass` `Algebra.id` `UniformConvergenceCLM.instModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `equivWeakDual`	—	`RingHomInvPair.ids` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Algebra.to_smulCommClass`
`evalCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem` `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` `evalCLM`	—	`smulCommClass_self`
`hasBasis_nhds_zero` 📖	mathematical	—	`Filter.HasBasis` `PointwiseConvergenceCLM` `Set` `nhds` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Finite` `Set.Elem` `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`	`Filter.HasBasis` `PointwiseConvergenceCLM` `Set` `nhds` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Finite` `Set.Elem` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup`	—	`UniformConvergenceCLM.hasBasis_nhds_zero_of_basis` `Set.finite_empty` `directedOn_of_sup_mem` `Set.Finite.union`
`instT2Space` 📖	mathematical	—	`T2Space` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem`	—	`UniformConvergenceCLM.t2Space` `Set.sUnion_finite_eq_univ`
`isEmbedding_coeFn` 📖	mathematical	—	`Topology.IsEmbedding` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem` `Pi.topologicalSpace` `DFunLike.coe` `UniformConvergenceCLM.instFunLike`	—	`isUniformAddGroup_of_addCommGroup` `IsUniformEmbedding.isEmbedding` `isUniformEmbedding_coeFn`
`isUniformEmbedding_coeFn` 📖	mathematical	—	`IsUniformEmbedding` `PointwiseConvergenceCLM` `UniformSpace.toTopologicalSpace` `UniformConvergenceCLM.instUniformSpace` `setOf` `Set` `Finite` `Set.Elem` `Pi.uniformSpace` `DFunLike.coe` `UniformConvergenceCLM.instFunLike`	—	`IsUniformEmbedding.comp` `UniformOnFun.isUniformEmbedding_toFun_finite` `UniformConvergenceCLM.isUniformEmbedding_coeFn`
`postcomp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem` `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` `postcomp` `ContinuousLinearMap.comp`	—	`smulCommClass_self`
`precomp_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `PointwiseConvergenceCLM` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem` `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` `precomp` `ContinuousLinearMap.comp`	—	`smulCommClass_self`
`tendsto_iff_forall_tendsto` 📖	mathematical	—	`Filter.Tendsto` `PointwiseConvergenceCLM` `nhds` `UniformConvergenceCLM.instTopologicalSpace` `setOf` `Set` `Finite` `Set.Elem` `DFunLike.coe` `UniformConvergenceCLM.instFunLike`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding_coeFn`

(root)

Definitions

Name	Category	Theorems
`PointwiseConvergenceCLM` 📖	CompOp	21 math math: `PointwiseConvergenceCLM.continuous_of_continuous_eval`, `PointwiseConvergenceCLM.tendsto_nhds`, `PointwiseConvergenceCLM.postcomp_apply`, `PointwiseConvergenceCLM.instLocallyConvexSpace`, `PointwiseConvergenceCLM.instT2Space`, `PointwiseConvergenceCLM.isEmbedding_coeFn`, `PointwiseConvergenceCLM.isInducing_inducingFn`, `PointwiseConvergenceCLM.equivWeakDual_apply`, `PointwiseConvergenceCLM.equivWeakDual_symm_apply`, `PointwiseConvergenceCLM.coeLMₛₗ_apply`, `PointwiseConvergenceCLM.continuousEvalConst`, `PointwiseConvergenceCLM.coeLM_apply`, `PointwiseConvergenceCLM.precomp_apply`, `PointwiseConvergenceCLM.tendsto_nhds_atTop`, `PointwiseConvergenceCLM.tendsto_iff_forall_tendsto`, `PointwiseConvergenceCLM.hasBasis_nhds_zero`, `PointwiseConvergenceCLM.evalCLM_apply`, `PointwiseConvergenceCLM.withSeminorms`, `PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis`, `ContinuousLinearMap.toPointwiseConvergenceCLM_apply`, `PointwiseConvergenceCLM.isUniformEmbedding_coeFn`
`«term_→Lₚₜ[_]_»` 📖	CompOp	—
`«term_→SLₚₜ[_]_»` 📖	CompOp	—

---

← Back to Index