TsumUniformlyOn

📁 Source: Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean

Statistics

Metric	Count
Definitions	0
Theorems of_norm_le_summable, of_norm_le_summable_eventually, of_locally_bounded_eventually, SummableLocallyUniformlyOn_of_locally_bounded, derivWithin_tsum, iteratedDerivWithin_tsum	6
Total	6

HasSumUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_norm_le_summable 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	HasSumUniformlyOn ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid tsum	—	tendstoUniformlyOn_tsum
of_norm_le_summable_eventually 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	HasSumUniformlyOn ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid tsum	—	tendstoUniformlyOn_tsum_of_cofinite_eventually

SummableLocallyUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_locally_bounded_eventually 📖	mathematical	IsOpen Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.cofinite	SummableLocallyUniformlyOn ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	HasSumLocallyUniformlyOn.summableLocallyUniformlyOn hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn tendstoLocallyUniformlyOn_iff_forall_isCompact tendstoUniformlyOn_tsum_of_cofinite_eventually

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SummableLocallyUniformlyOn_of_locally_bounded 📖	mathematical	IsOpen Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	SummableLocallyUniformlyOn ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	SummableLocallyUniformlyOn.of_locally_bounded_eventually Filter.univ_mem'
derivWithin_tsum 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set Set.instMembership Summable ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SummationFilter.unconditional SummableLocallyUniformlyOn derivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DifferentiableAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace	tsum	—	HasDerivWithinAt.derivWithin HasDerivAt.hasDerivWithinAt hasDerivAt_of_tendstoLocallyUniformlyOn SummationFilter.instNeBotFinsetFilterOfNeBot SummationFilter.instNeBotUnconditional TendstoLocallyUniformlyOn.congr_right hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn HasSumLocallyUniformlyOn.tsum_eqOn TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.univ_mem' IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.fun_sum HasDerivWithinAt.hasDerivAt DifferentiableWithinAt.hasDerivWithinAt DifferentiableAt.differentiableWithinAt IsOpen.mem_nhds Summable.hasSum IsOpen.uniqueDiffWithinAt PerfectSpace.not_isolated instPerfectSpace ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd
iteratedDerivWithin_tsum 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Set Set.instMembership Summable ESeminormedAddCommMonoid.toAddCommMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SummationFilter.unconditional SummableLocallyUniformlyOn iteratedDerivWithin DifferentiableAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace	tsum	—	iteratedDerivWithin_zero iteratedDerivWithin_succ derivWithin_tsum Summable.congr SummableLocallyUniformlyOn.summable SummableLocallyUniformlyOn_congr derivWithin_congr

---

← Back to Index