Documentation Verification Report

SummableUniformlyOn

📁 Source: Mathlib/Analysis/Complex/SummableUniformlyOn.lean

Statistics

Metric	Count
Definitions `SummableUniformlyOn`	1
Theorems `differentiableOn`	1
Total	2

SummableLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableOn` 📖	mathematical	`IsOpen` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `CommCStarAlgebra.toNormedCommRing` `instCommCStarAlgebraComplex` `SummableLocallyUniformlyOn` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DifferentiableAt` `DenselyNormedField.toNontriviallyNormedField` `Complex.instDenselyNormedField` `Complex.addCommGroup` `Complex.instModuleSelf` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Complex.instNormedField`	`DifferentiableOn` `tsum` `SummationFilter.unconditional`	—	`TendstoLocallyUniformlyOn.differentiableOn` `Filter.atTop_neBot` `Finset.isDirected_le` `hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` `Filter.univ_mem'` `DifferentiableWithinAt.fun_sum` `DifferentiableAt.differentiableWithinAt` `DifferentiableOn.congr` `HasSumLocallyUniformlyOn.tsum_eqOn` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`

(root)

Definitions

Name	Category	Theorems
`SummableUniformlyOn` 📖	MathDef	4 math math: `SummableUniformly.summableUniformlyOn`, `HasSumUniformlyOn.summableUniformlyOn`, `summableUniformlyOn_iff_hasSumUniformlyOn`, `summableUniformlyOn_univ_iff`

---

← Back to Index