FunctionSeries

📁 Source: Mathlib/Analysis/Normed/Group/FunctionSeries.lean

Statistics

Metric	Count
Definitions	0
Theorems continuousOn_tsum, continuous_tsum, tendstoUniformlyOn_tsum, tendstoUniformlyOn_tsum_nat, tendstoUniformlyOn_tsum_nat_eventually, tendstoUniformlyOn_tsum_of_cofinite_eventually, tendstoUniformly_tsum, tendstoUniformly_tsum_nat, tendstoUniformly_tsum_of_cofinite_eventually	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_tsum 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Summable Real Real.instAddCommMonoid Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	TendstoUniformlyOn.continuousOn tendstoUniformlyOn_tsum Filter.Frequently.of_forall Filter.atTop_neBot Finset.isDirected_le continuousOn_finset_sum IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup
continuous_tsum 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Summable Real Real.instAddCommMonoid Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	continuousOn_tsum
tendstoUniformlyOn_tsum 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	TendstoUniformlyOn Finset SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid tsum Filter.atTop PartialOrder.toPreorder Finset.partialOrder	—	Metric.tendstoUniformlyOn_iff Filter.mp_mem tendsto_order instOrderTopologyReal tendsto_tsum_compl_atTop_zero instIsTopologicalAddGroupReal Filter.univ_mem' Summable.of_nonneg_of_le norm_nonneg dist_eq_norm Summable.sum_add_tsum_subtype_compl SeminormedAddCommGroup.to_isUniformAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Summable.of_norm add_sub_cancel_left lt_of_le_of_lt LE.le.trans norm_tsum_le_tsum_norm Summable.subtype instIsUniformAddGroupReal Real.instCompleteSpace Summable.tsum_le_tsum Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology SummationFilter.instNeBotUnconditional
tendstoUniformlyOn_tsum_nat 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	TendstoUniformlyOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.range tsum Filter.atTop Nat.instPreorder	—	Filter.Tendsto.eventually Filter.tendsto_finset_range tendstoUniformlyOn_tsum
tendstoUniformlyOn_tsum_nat_eventually 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Nat.instPreorder	TendstoUniformlyOn SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.range tsum	—	Filter.Tendsto.eventually Filter.tendsto_finset_range tendstoUniformlyOn_tsum_of_cofinite_eventually Nat.cofinite_eq_atTop
tendstoUniformlyOn_tsum_of_cofinite_eventually 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	TendstoUniformlyOn Finset SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid tsum Filter.atTop PartialOrder.toPreorder Finset.partialOrder	—	Metric.tendstoUniformlyOn_iff tendsto_order instOrderTopologyReal tendsto_tsum_compl_atTop_zero instIsTopologicalAddGroupReal Finset.isDirected_le Filter.eventually_iff_exists_mem Summable.add_compl IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Summable.of_finite Finite.of_fintype SummationFilter.instHasSupportOfLeAtTop SummationFilter.instLeAtTopUnconditional Summable.of_nonneg_of_le norm_nonneg Summable.subtype instIsUniformAddGroupReal Real.instCompleteSpace dist_eq_norm Summable.sum_add_tsum_subtype_compl SeminormedAddCommGroup.to_isUniformAddGroup TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Summable.of_norm add_sub_cancel_left lt_of_le_of_lt LE.le.trans norm_tsum_le_tsum_norm Summable.tsum_le_tsum Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology SummationFilter.instNeBotUnconditional Finset.union_subset_left Finset.union_subset_right
tendstoUniformly_tsum 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	TendstoUniformly Finset SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid tsum Filter.atTop PartialOrder.toPreorder Finset.partialOrder	—	tendstoUniformlyOn_univ tendstoUniformlyOn_tsum
tendstoUniformly_tsum_nat 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Real.instLE Norm.norm NormedAddCommGroup.toNorm	TendstoUniformly SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.range tsum Filter.atTop Nat.instPreorder	—	Filter.Tendsto.eventually Filter.tendsto_finset_range tendstoUniformly_tsum
tendstoUniformly_tsum_of_cofinite_eventually 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	TendstoUniformly Finset SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid tsum Filter.atTop PartialOrder.toPreorder Finset.partialOrder	—	tendstoUniformlyOn_univ tendstoUniformlyOn_tsum_of_cofinite_eventually

---

← Back to Index