Theorems · Theorem · sequences and series

cauchySeq_of_edist_le_geometric

∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal),
  r < 1 → C ≠ ⊤ → ∀ {f : ℕ → α}, (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) → CauchySeq f

If edist (f n) (f (n+1)) is bounded by C * r^n, C ≠ ∞, r < 1, then f is a Cauchy sequence.

Defined in

Mathlib.Analysis.SpecificLimits.Basic

Cited by

2 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace