Documentation
LeanCourse
.
MIL
.
C10_Topology
.
S02_Metric_Spaces
Search
Google site search
return to top
source
Imports
Init
LeanCourse.Common
Mathlib.Topology.Instances.Real
Mathlib.Analysis.Normed.Operator.BanachSteinhaus
Imported by
cauchySeq_of_le_geometric_two'
source
theorem
cauchySeq_of_le_geometric_two'
{X :
Type
u_1}
[
MetricSpace
X
]
{u :
ℕ
→
X
}
(hu :
∀ (
n
:
ℕ
),
dist
(
u
n
)
(
u
(
n
+
1
)
)
≤
(
1
/
2
)
^
n
)
:
CauchySeq
u