Documentation

LeanCourse.MIL.C10_Topology.S02_Metric_Spaces

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) :