Real

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

Statistics

Metric	Count
Definitions	0
Theorems tsum_le_of_sum_le, tsum_le_of_sum_range_le, tsum_lt_tsum_of_nonneg, cauchySeq_of_dist_le_of_summable, cauchySeq_of_summable_dist, dist_le_tsum_dist_of_tendsto, dist_le_tsum_dist_of_tendsto₀, dist_le_tsum_of_dist_le_of_tendsto, dist_le_tsum_of_dist_le_of_tendsto₀, not_summable_iff_tendsto_nat_atTop_of_nonneg, summable_iff_not_tendsto_nat_atTop_of_nonneg, summable_of_sum_le, summable_of_sum_range_le, summable_partition, summable_prod_of_nonneg, summable_sigma_of_nonneg	16
Total	16

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tsum_le_of_sum_le 📖	mathematical	Pi.hasLe Real instLE Pi.instZero instZero Finset.sum instAddCommMonoid	tsum UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SummationFilter.unconditional	—	Summable.tsum_le_of_sum_le OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotUnconditional summable_of_sum_le
tsum_le_of_sum_range_le 📖	mathematical	Real instLE instZero Finset.sum instAddCommMonoid Finset.range	tsum UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace SummationFilter.unconditional	—	Summable.tsum_le_of_sum_range_le instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal summable_of_sum_range_le

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tsum_lt_tsum_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero Real.instLT Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	tsum	—	tsum_lt_tsum Real.instIsOrderedAddMonoid instIsTopologicalAddGroupReal OrderTopology.to_orderClosedTopology instOrderTopologyReal SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional of_nonneg_of_le

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_of_dist_le_of_summable 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	CauchySeq Nat.instPreorder	—	CanLift.prf Pi.canLift NNReal.canLift LE.le.trans dist_nonneg cauchySeq_of_edist_le_of_summable
cauchySeq_of_summable_dist 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist SummationFilter.unconditional	CauchySeq Nat.instPreorder	—	cauchySeq_of_dist_le_of_summable le_rfl
dist_le_tsum_dist_of_tendsto 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist SummationFilter.unconditional Filter.Tendsto Filter.atTop Nat.instPreorder nhds	Real.instLE tsum	—	dist_le_tsum_of_dist_le_of_tendsto le_rfl
dist_le_tsum_dist_of_tendsto₀ 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Dist.dist PseudoMetricSpace.toDist SummationFilter.unconditional Filter.Tendsto Filter.atTop Nat.instPreorder nhds	Real.instLE tsum	—	zero_add dist_le_tsum_dist_of_tendsto
dist_le_tsum_of_dist_le_of_tendsto 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Tendsto Filter.atTop Nat.instPreorder nhds	tsum	—	le_of_tendsto instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.dist tendsto_const_nhds Filter.eventually_atTop le_trans dist_le_Ico_sum_of_dist_le Finset.sum_Ico_eq_sum_range Summable.sum_le_tsum Real.instIsOrderedAddMonoid SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional dist_nonneg Summable.comp_injective instIsUniformAddGroupReal Real.instCompleteSpace add_right_injective AddLeftCancelSemigroup.toIsLeftCancelAdd
dist_le_tsum_of_dist_le_of_tendsto₀ 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Tendsto Filter.atTop Nat.instPreorder nhds	tsum	—	zero_add dist_le_tsum_of_dist_le_of_tendsto
not_summable_iff_tendsto_nat_atTop_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Tendsto Finset.sum Finset.range Filter.atTop Nat.instPreorder Real.instPreorder	—	CanLift.prf Pi.canLift NNReal.canLift Finset.sum_congr NNReal.not_summable_iff_tendsto_nat_atTop
summable_iff_not_tendsto_nat_atTop_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Tendsto Finset.sum Finset.range Filter.atTop Nat.instPreorder Real.instPreorder	—	not_iff_not not_summable_iff_tendsto_nat_atTop_of_nonneg
summable_of_sum_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Finset.sum Real.instAddCommMonoid	Summable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	—	tendsto_atTop_ciSup LinearOrder.supConvergenceClass instOrderTopologyReal Finset.sum_mono_set_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
summable_of_sum_range_le 📖	mathematical	Real Real.instLE Real.instZero Finset.sum Real.instAddCommMonoid Finset.range	Summable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	—	summable_iff_not_tendsto_nat_atTop_of_nonneg Filter.exists_lt_of_tendsto_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial lt_irrefl LT.lt.trans_le
summable_partition 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero ExistsUnique Set Set.instMembership	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Set.Elem tsum	—	Equiv.summable_iff summable_sigma_of_nonneg
summable_prod_of_nonneg 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional tsum	—	Equiv.summable_iff summable_sigma_of_nonneg
summable_sigma_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional tsum	—	CanLift.prf Pi.canLift NNReal.canLift NNReal.summable_sigma

---

← Back to Index