Theorems · Theorem · general topology
tendsto_nhds_unique
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [l.NeBot],
Filter.Tendsto f l (nhds a) → Filter.Tendsto f l (nhds b) → a = b- Defined in
- Mathlib.Topology.Separation.Hausdorff
- Cited by
- 118 results in Mathlib
- Foundations
- Depth 90 from the axioms, rests on 1,970 definitions · uses propext, Classical.choice, Quot.sound
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.
- TopologicalSpacestatement and proof · cited by 24,529
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- T2Spacestatement and proof · cited by 1,351
- Filter.NeBotstatement and proof · cited by 853
- Inseparable.eqproof · cited by 19
- tendsto_nhds_unique_inseparableproof · cited by 10
Cited by118
Results whose statement or proof uses this declaration.
- HasSum.uniqueproof · cited by 23
- tendsto_nhds_unique_of_eventuallyEqproof · cited by 13
- StieltjesFunction.measure_Iicproof · cited by 8
- Complex.exp_eq_exp_ℂproof · cited by 8
- IsSelfAdjoint.spectralRadius_eq_nnnormproof · cited by 7
- MeasureTheory.integral_trimproof · cited by 6
- Hyperreal.IsSt.uniqueproof · cited by 6
- StieltjesFunction.measure_singletonproof · cited by 6
- lim_eqproof · cited by 6
- ContDiffWithinAt.isSymmSndFDerivWithinAtproof · cited by 6
- MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendstoproof · cited by 5
- StieltjesFunction.measure_univproof · cited by 5