Convergent_Sequence_in_Hausdorff_Space_has_Unique_Limit

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

hausdorff-spaceslimits-of-sequencesproofwiki

Let $T = \struct {S, \tau}$ be a Hausdorff space. Let $\sequence {x_n}$ be a convergent sequence in $T$ . Then $\sequence {x_n}$ has exactly one limit.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Convergent_Sequence_in_Hausdorff_Space_has_Unique_Limit {α : Type _} [TopologicalSpace α] [T2Space α] {f : ℕ → α} {a b : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) (hb : Filter.Tendsto f Filter.atTop (nhds b)) : a = b := by sorry

Source

https://proofwiki.org/wiki/Convergent_Sequence_in_Hausdorff_Space_has_Unique_Limit

View graph