Theorems · Theorem · sequences and series

dist_le_tsum_of_dist_le_of_tendsto

∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ),
  (∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) →
    Summable d → ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Defined in: Mathlib.Topology.Algebra.InfiniteSum.Real
Cited by: 4 results in Mathlib
Foundations: Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

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
nhdsstatement and proof · cited by 5,554
Filter.Tendstostatement and proof · cited by 3,814
Filter.atTopstatement and proof · cited by 2,405
SummationFilter.unconditionalstatement and proof · cited by 2,068
PseudoMetricSpacestatement and proof · cited by 1,550
Dist.diststatement and proof · cited by 1,539
Finset.rangeproof · cited by 1,341
tsumstatement and proof · cited by 1,148
le_transproof · cited by 985
Summablestatement and proof · cited by 778
tendsto_const_nhdsproof · cited by 330

Cited by4

Results whose statement or proof uses this declaration.

dist_le_tsum_of_dist_le_of_tendsto₀proof · cited by 2
dist_le_of_le_geometric_of_tendstoproof · cited by 1
dist_le_tsum_dist_of_tendstoproof · cited by 1
dist_le_of_le_geometric_two_of_tendstoproof · cited by 0