no goals
K : Type u_1
E : Type ?u.7229030
inst✝ : IsROrC K
f : CauSeq K norm
ε : ℝ
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → ‖↑f j - ↑f i‖ < ε
j : ℕ
ij : j ≥ i
⊢ abs ((fun n => ↑im (↑f n)) j - (fun n => ↑im (↑f n)) i) ≤ ‖↑f j - ↑f i‖
simpa only [map_sub] using abs_im_le_norm (f j - f i)