Theorems · Theorem · general topology
dist_le_Ico_sum_dist
∀ {α : Type u} [inst : PseudoMetricSpace α] (f : ℕ → α) {m n : ℕ},
m ≤ n → dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))The triangle (polygon) inequality for sequences of points; Finset.Ico version.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 103 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.
Cites17
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
- Finsetproof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- le_reflproof · cited by 2,061
- le_rflproof · cited by 1,558
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement and proof · cited by 1,539
- add_commproof · cited by 1,535
- add_le_addproof · cited by 666
- Finset.Icostatement and proof · cited by 450
- Finset.sum_insertproof · cited by 196
- dist_selfproof · cited by 116
Cited by2
Results whose statement or proof uses this declaration.
- dist_le_range_sum_distproof · cited by 2
- dist_le_Ico_sum_of_dist_leproof · cited by 2