Theorems · Theorem · general topology
dist_le_range_sum_of_dist_le
∀ {α : Type u} [inst : PseudoMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ},
(∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k) → dist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d iA version of dist_le_range_sum_dist with each intermediate distance replaced
with an upper estimate.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finset.sumstatement · cited by 5,195
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement and proof · cited by 1,539
- Finset.rangestatement · cited by 1,341
- zero_leproof · cited by 382
- Nat.Ico_zero_eq_rangeproof · cited by 25
- dist_le_Ico_sum_of_dist_leproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWithproof · cited by 1
- ODE.FunSpace.dist_iterate_next_leproof · cited by 1