intro δ hδ
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hcheby : cheby fun n => ↑(f n)
⊢ ∀ ε > 0, ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < ε
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hcheby : cheby fun n => ↑(f n)
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (n : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (S f 0 n.2) (S f n.1 n.2) < δ