uniqueness of limit

Stream: new members

[Heather Macbeth]

What files would facts like this be in? library_search fails, presumably it's a combination of a couple of existing lemmas.

example {f : ℕ → ℝ} {a₁ a₂ : ℝ}
  (h₁ : filter.tendsto f filter.at_top (nhds a₁)) (h₂ : filter.tendsto f filter.at_top (nhds a₂)) :
  a₁ = a₂

[Alex J. Best]

There is docs#tendsto_nhds_unique in topology/separation.lean , does that help?

[Patrick Massot]

tendsto_nhds_unique at_top_ne_bot h₁ h₂

[Patrick Massot]

You need to open filter of course.

[Heather Macbeth]

Thanks!