α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ (∑' (n : ℕ), C * r ^ n) ≠ ⊤
α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f
refine' cauchySeq_of_edist_le_of_tsum_ne_top _ hu _
α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ C * (1 - r)⁻¹ ≠ ⊤
α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ (∑' (n : ℕ), C * r ^ n) ≠ ⊤
rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ 1 - r ≠ 0
α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ C * (1 - r)⁻¹ ≠ ⊤
refine' ENNReal.mul_ne_top hC (ENNReal.inv_ne_top.2 _)
no goals
α : Type u_1
β : Type ?u.430769
ι : Type ?u.430772
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ 1 - r ≠ 0
exact (tsub_pos_iff_lt.2 hr).ne'