Tannery

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

Statistics

Metric	Count
Definitions	0
Theorems tendsto_tsum_of_dominated_convergence	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_tsum_of_dominated_convergence 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Tendsto nhds SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Filter.Eventually	tsum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	isEmpty_or_nonempty tsum_empty tendsto_const_nhds Filter.eq_or_neBot le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.Tendsto.comp tendsto_norm Filter.Eventually.mono Summable.of_norm_bounded Real.instCompleteSpace norm_norm Filter.mp_mem Filter.univ_mem' Metric.tendsto_nhds Nat.instAtLeastTwoHAddOfNat Filter.Eventually.exists SummationFilter.instNeBotFinsetFilterOfNeBot SummationFilter.instNeBotUnconditional HasSum.eq_1 div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.le_norm_self Summable.sum_add_tsum_compl instIsTopologicalAddGroupReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace HasSum.tsum_eq norm_sub_rev dist_eq_norm tendsto_finset_sum IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Summable.tsum_sub Summable.of_norm Summable.sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat LE.le.trans_lt norm_add_le add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Finset.sum_sub_distrib Summable.subtype instIsUniformAddGroupReal norm_sub_le LE.le.trans norm_tsum_le_tsum_norm Summable.tsum_le_tsum

---

← Back to Index