Documentation Verification Report

Completeness

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_subseq_summable_dist_of_cauchySeq`, `completeSpace_of_summable_imp_tendsto`, `summable_imp_tendsto_iff_completeSpace`, `summable_imp_tendsto_of_complete`	4
Total	4

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_subseq_summable_dist_of_cauchySeq` 📖	mathematical	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `Nat.instPreorder`	`StrictMono` `Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `Real.pseudoMetricSpace` `Dist.dist` `PseudoMetricSpace.toDist` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_subseq_bounded_of_cauchySeq` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `Summable.of_nonneg_of_le` `dist_nonneg` `le_of_lt` `StrictMono.monotone` `summable_geometric_two`

NormedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace_of_summable_imp_tendsto` 📖	mathematical	`Filter.Tendsto` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `toENormedAddCommMonoid` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds`	`CompleteSpace`	—	`Metric.complete_of_cauchySeq_tendsto` `Metric.exists_subseq_summable_dist_of_cauchySeq` `Finset.sum_range_sub` `dist_eq_norm` `tendsto_nhds_of_cauchySeq_of_subseq` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `StrictMono.tendsto_atTop` `Filter.Tendsto.add_const` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `sub_add_cancel`
`summable_imp_tendsto_iff_completeSpace` 📖	mathematical	—	`Filter.Tendsto` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `toENormedAddCommMonoid` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds` `CompleteSpace`	—	`completeSpace_of_summable_imp_tendsto` `summable_imp_tendsto_of_complete`
`summable_imp_tendsto_of_complete` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `toNorm` `SummationFilter.unconditional`	`Filter.Tendsto` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `toENormedAddCommMonoid` `Finset.range` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`cauchySeq_tendsto_of_complete` `cauchySeq_of_summable_dist` `Finset.sum_range_succ` `dist_eq_norm` `sub_add_cancel_left` `norm_neg`

---

← Back to Index