Documentation Verification Report

PointwiseConvergence

📁 Source: Mathlib/Analysis/LocallyConvex/PointwiseConvergence.lean

Statistics

Metric	Count
Definitions `inducingFn`, `mkCLM`, `seminorm`, `seminormFamily`	4
Theorems `instLocallyConvexSpace`, `isInducing_inducingFn`, `tendsto_nhds`, `tendsto_nhds_atTop`, `withSeminorms`	5
Total	9

PointwiseConvergenceCLM

Definitions

Name	Category	Theorems
`inducingFn` 📖	CompOp	1 math math: `isInducing_inducingFn`
`mkCLM` 📖	CompOp	—
`seminorm` 📖	CompOp	—
`seminormFamily` 📖	CompOp	1 math math: `withSeminorms`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLocallyConvexSpace` 📖	mathematical	—	`LocallyConvexSpace` `PointwiseConvergenceCLM` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `setOf` `Set` `Finite` `Set.Elem` `UniformConvergenceCLM.instModule` `UniformConvergenceCLM.instTopologicalSpace`	—	`UniformConvergenceCLM.locallyConvexSpace` `Set.finite_empty` `directedOn_of_sup_mem` `Set.Finite.union`
`isInducing_inducingFn` 📖	mathematical	—	`Topology.IsInducing` `PointwiseConvergenceCLM` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Set` `Finite` `Set.Elem` `Pi.topologicalSpace` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `UniformConvergenceCLM.instAddCommGroup` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniformConvergenceCLM.instModule` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Pi.Function.module` `LinearMap.instFunLike` `inducingFn`	—	`Topology.IsEmbedding.isInducing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `isEmbedding_coeFn`
`tendsto_nhds` 📖	mathematical	—	`Filter.Tendsto` `PointwiseConvergenceCLM` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `nhds` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Set` `Finite` `Set.Elem` `Filter.Eventually` `Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `UniformConvergenceCLM.instFunLike`	—	`WithSeminorms.tendsto_nhds` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `withSeminorms`
`tendsto_nhds_atTop` 📖	mathematical	—	`Filter.Tendsto` `PointwiseConvergenceCLM` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `UniformConvergenceCLM.instTopologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Set` `Finite` `Set.Elem` `Real` `Real.instLT` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `DFunLike.coe` `UniformConvergenceCLM.instFunLike`	—	`WithSeminorms.tendsto_nhds_atTop` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `withSeminorms`
`withSeminorms` 📖	mathematical	—	`WithSeminorms` `PointwiseConvergenceCLM` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `UniformConvergenceCLM.instAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `setOf` `Set` `Finite` `Set.Elem` `UniformConvergenceCLM.instModule` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `NormedField.toField` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Module.toDistribMulAction` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `seminormFamily` `UniformConvergenceCLM.instTopologicalSpace`	—	`Topology.IsInducing.withSeminorms` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `WithSeminorms.congr_equiv` `withSeminorms_pi` `norm_withSeminorms` `isInducing_inducingFn`

---

← Back to Index