theorem Sequences.special_sequences : (∀ (p : ℝ), 0 < p → Filter.Tendsto (fun (n : ℕ) => ↑n ^ (-p)) Filter.atTop (nhds 0)) ∧ (∀ (p : ℝ), 0 < p → Filter.Tendsto (fun (n : ℕ) => p ^ (1 / ↑n)) Filter.atTop (nhds 1)) ∧ Filter.Tendsto (fun (n : ℕ) => ↑n ^ (1 / ↑n)) Filter.atTop (nhds 1)

Some special sequences:

1. If p > 0, then n^(-p) → 0 as n → ∞.
2. If p > 0, then p^(1/n) → 1 as n → ∞.
3. n^(1/n) → 1 as n → ∞.