Bijections and Inverses, Cauchy sequence permutations

Stream: Is there code for X?

[Yury G. Kudryashov]

We have docs#filter.tendsto.comp

[Yury G. Kudryashov]

So you have

example {α : Type*} [topological_space α] {u : ℕ → α} {a : α} (hu : tendsto u at_top (𝓝 a))
  {f : ℕ → ℕ} (hf : function.injective f) : tendsto (u ∘ f) at_top (𝓝 a) :=
hu.comp hf.tendsto_at_top

[Yury G. Kudryashov]

I don't think that we should add this as a separate lemma.

[Kevin Buzzard]

@Mark Gerads what's going on here is that the lemma you're proving is just the sort of thing which we see in undergraduate analysis textbooks, but in fact it's an easy consequence of a far more general lemma about filters on uniform spaces and mathlib is focused on proving things in this kind of large generality. Mathlib is not designed for pedagogy, it is like Bourbaki, striving for maximal generality rather than concrete examples such as your application

[Kevin Buzzard]

The very fact that you want to state the lemma for both real and complex sequences is exactly the reason we state it for neither. Next week someone will want it for sequences of p-adic numbers, the week after someone will want it for ℝ^3 etc

[Mark Gerads]

Oh, I definitely support having every proof as general as possible. I am glad that [a much more general proof than what I had in mind] was submitted to mathlib.