α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ m ∈ {x | (fun c => edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}
α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)
refine' le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => _⟩)
α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i in Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ m ∈ {x | (fun c => edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}
refine' le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) _
α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k in Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i in Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
rw [Finset.sum_Ico_eq_sum_range]
no goals
α : Type u_1
β : Type ?u.567007
γ : Type ?u.567010
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k in Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
exact sum_le_tsum _ (fun _ _ => zero_le _) ENNReal.summable