Theorems · Theorem · general topology
tendsto_iff_edist_tendsto_0
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] {l : Filter β} {f : β → α} {y : α},
Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (fun x => edist (f x) y) l (nhds 0)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Filterstatement and proof · cited by 8,121
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- Filter.Eventuallyproof · cited by 3,134
- PseudoEMetricSpacestatement and proof · cited by 1,536
- OrderTopologyproof · cited by 1,355
- EDist.ediststatement and proof · cited by 735
- Filter.HasBasis.tendsto_right_iffproof · cited by 81
- tendsto_orderproof · cited by 60
- Metric.nhds_basis_eballproof · cited by 10
- ENNReal.not_lt_zeroproof · cited by 5
Cited by2
Results whose statement or proof uses this declaration.
- tendsto_iff_enorm_neg_add_tendsto_zeroproof · cited by 1
- tendsto_iff_enorm_sub_tendsto_zeroproof · cited by 0