case intro
α : Type u_1
β : Type ?u.428595
γ : Type ?u.428598
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ (fun i => ↑(d i)) n
hd : (∑' (i : ℕ), ↑(d i)) ≠ ⊤
⊢ CauchySeq f
α : Type u_1
β : Type ?u.428595
γ : Type ?u.428598
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ d n
hd : tsum d ≠ ⊤
⊢ CauchySeq f
lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i
case intro
α : Type u_1
β : Type ?u.428595
γ : Type ?u.428598
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => d i
⊢ CauchySeq f
case intro
α : Type u_1
β : Type ?u.428595
γ : Type ?u.428598
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ (fun i => ↑(d i)) n
hd : (∑' (i : ℕ), ↑(d i)) ≠ ⊤
⊢ CauchySeq f
rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd
no goals
case intro
α : Type u_1
β : Type ?u.428595
γ : Type ?u.428598
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ (fun i => ↑(d i)) n
hd : Summable fun i => d i
⊢ CauchySeq f
exact cauchySeq_of_edist_le_of_summable d hf hd