metric space equal elements

Stream: new members

[Patrick Lutz]

What's the quickest way to prove that in a metric space, if the same sequence converges to two separate things then those things are equal? I can prove it, but I feel like there should just be some theorem in mathlib that does it (but I haven't been able to find such a thing via library_search or a manual scan of the relevant parts of mathlib). MWE:

import topology.metric_space.basic

universe u
variables {X : Type u} [metric_space X]

example (x : ℕ → X) (y z : X) : (filter.tendsto x filter.at_top (nhds y))
     → (filter.tendsto x filter.at_top (nhds z)) → y = z := sorry

[Reid Barton]

let's see if this works: docs#tendsto_nhds_unique

[Patrick Lutz]

Oh, nice

[Patrick Lutz]

I somehow missed the existence of topology.separation

[Patrick Lutz]

Is there some way you found that so quickly? I definitely feel like things often take me lots of time in Lean just because I have trouble quickly finding the relevant theorems in mathlib

[Reid Barton]

I've used it before and I remembered the place where I used it :upside_down:

[Patrick Lutz]

Okay, I was hoping that there was some big secret I was just missing, but that makes sense