names?

Stream: maths

[Yury G. Kudryashov]

Hi, what would be a good name for the following lemmas?

lemma TODO1 {α β : Type*} [semilattice_sup β] [nonempty β]
  {l : filter α} (hl : has_countable_basis l)
  {x : ℕ → β → α} (hx : ∀ s ∈ l, ∀ᶠ k n in at_top, x k n ∈ s) :
  ∀ᶠ (N : ℕ → β) in at_top, tendsto (λ k, x k (N k)) at_top l := sorry

lemma TODO2 {α : Type*} [topological_space α] [first_countable_topology α]
  {x : ℕ → ℕ → α} {y : ℕ → α} {z : α}
  (hx : ∀ᶠ k in at_top, tendsto (x k) at_top (𝓝 (y k))) (hy : tendsto y at_top (𝓝 z)) :
  ∀ᶠ (N : ℕ → ℕ) in at_top, tendsto (λ k, x k (N k)) at_top (𝓝 z) := sorry

lemma TODO3 {α : Type*} {l : filter α} (hl : has_countable_basis l)
  {x : ℕ → ℕ → α} (hx : ∀ᶠ k in at_top, tendsto (x k) at_top l) :
  ∀ᶠ (N : ℕ → ℕ) in at_top, tendsto (λ k, x k (N k)) at_top l := sorry

The main lemma TODO1 and its particular cases TODO2 and TODO3 formalize the following common practice. Consider a sequence of sequences x : ℕ → ℕ → α. Suppose that each x k has a limit y k (either finite or infinite), and these limits converge to z. Then x k (n k) tends to z provided that n k tends to infinity sufficiently fast.

[Sebastien Gouezel]

tendsto_of_tendsto_of_tendsto_of_sufficiently_fast_growth for the second one?

I didn't know that ∀ᶠ (N : ℕ → β) in at_top makes sense, i.e., that there is an at_top filter on ℕ → β. I think these lemmas will need ample docstrings to explain what is going on :)