theorem isConnected_clusterPoints_of_tendsto_dist_succ_eq_zero {X : Type u} [MetricSpace X] {C : Set X} {u : ℕ → X} (hC : IsCompact C) (huC : ∀ (n : ℕ), u n ∈ C) (hstep : Filter.Tendsto (fun (n : ℕ) => dist (u n) (u (n + 1))) Filter.atTop (nhds 0)) : IsConnected {x : X | MapClusterPt x Filter.atTop u}

Theorem 1.49: (Ostrowski) in a metric space, if C is compact, a sequence u takes values in C, and dist (u n) (u (n + 1)) → 0, then the cluster-point set of u is connected. Under the hypothesis u n ∈ C, every cluster point already lies in C, so this is equivalent to the textbook formulation with C ∩ {x | MapClusterPt x atTop u}.

theorem isConnected_clusterPointsIn_compact_of_tendsto_dist_succ_eq_zero {X : Type u} [MetricSpace X] {C : Set X} {u : ℕ → X} (hC : IsCompact C) (huC : ∀ (n : ℕ), u n ∈ C) (hstep : Filter.Tendsto (fun (n : ℕ) => dist (u n) (u (n + 1))) Filter.atTop (nhds 0)) : IsConnected {x : X | x ∈ C ∧ MapClusterPt x Filter.atTop u}

Theorem 1.49 in textbook form: under the same hypotheses, the cluster points of u lying in C form a connected set. This is a one-step restatement of isConnected_clusterPoints_of_tendsto_dist_succ_eq_zero.