Theorems · Theorem · general topology
Filter.Tendsto.cauchySeq
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [Nonempty β] {f : β → α} {x : α},
Filter.Tendsto f Filter.atTop (nhds x) → CauchySeq f- Defined in
- Mathlib.Topology.UniformSpace.Cauchy
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.atTopstatement and proof · cited by 2,405
- UniformSpacestatement and proof · cited by 2,040
- SemilatticeSupstatement and proof · cited by 785
- CauchySeqstatement · cited by 131
- Filter.Tendsto.cauchy_mapproof · cited by 1
Cited by20
Results whose statement or proof uses this declaration.
- cauchySeq_of_edist_le_of_summableproof · cited by 2
- Metric.isBounded_range_of_tendstoproof · cited by 2
- Monotone.cauchySeq_series_mul_of_tendsto_zero_of_boundedproof · cited by 2
- Summable.vanishingproof · cited by 2
- controlled_sum_of_mem_closureproof · cited by 2
- Multipliable.tprod_vanishingproof · cited by 1
- Multipliable.vanishingproof · cited by 1
- IsSeqCompact.totallyBoundedproof · cited by 1
- Summable.nat_tsum_vanishingproof · cited by 1
- cauchySeq_sum_of_eventually_eqproof · cited by 1
- Complex.abel_auxproof · cited by 1
- Summable.tsum_vanishingproof · cited by 1