Theorems · Theorem · general topology
nhds_eq_comap_uniformity
∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = Filter.comap (Prod.mk x) (uniformity α)- Defined in
- Mathlib.Topology.UniformSpace.Defs
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- UniformSpacestatement and proof · cited by 2,040
- uniformitystatement · cited by 765
- Filter.comapstatement · cited by 546
- UniformSpace.nhds_eq_comap_uniformityproof · cited by 3
Cited by19
Results whose statement or proof uses this declaration.
- nhds_basis_uniformity'proof · cited by 8
- UniformSpace.mem_nhds_iffproof · cited by 7
- Uniform.tendsto_nhds_rightproof · cited by 7
- UniformSpace.toTopologicalSpace_iInfproof · cited by 6
- mem_nhds_uniformity_iff_rightproof · cited by 4
- lebesgue_number_lemmaproof · cited by 4
- nhds_comap_distproof · cited by 3
- isOpen_iff_ball_subsetproof · cited by 3
- tendsto_prod_filter_iffproof · cited by 2
- nhdsWithin_eq_comap_uniformity_of_memproof · cited by 2
- UniformSpace.hausdorff.isClosed_setOfPred_totallyBoundedproof · cited by 2
- Filter.Tendsto.tendstoUniformlyOnFilter_constproof · cited by 2