## Stream: maths

### Topic: names?

#### Yury G. Kudryashov (Feb 10 2020 at 02:30):

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 (Feb 10 2020 at 08:19):

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 :)

Last updated: May 06 2021 at 19:30 UTC