Convergent_Sequence_in_Metric_Space_is_Bounded
Provedlimits-of-sequencesmetric-spacesproofwiki
Let M be a metric space. If a sequence in M converges to a limit l, then the sequence is bounded.
Preamble
import Mathlib.Topology.MetricSpace.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.MetricSpace.Basic
theorem Convergent_Sequence_in_Metric_Space_is_Bounded {X : Type _} [PseudoMetricSpace X] (x : ℕ → X) (l : X) (h : Filter.Tendsto x Filter.atTop (nhds l)) : Bornology.IsBounded (Set.range x) := by sorrySource