Theorems · Theorem · general topology
Metric.nhds_basis_ball
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α}, (nhds x).HasBasis (fun x => 0 < x) (Metric.ball x)- Defined in
- Mathlib.Topology.MetricSpace.Pseudo.Defs
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpace
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.
- Realstatement · cited by 25,697
- nhdsstatement · cited by 5,554
- PseudoMetricSpacestatement and proof · cited by 1,550
- Metric.ballstatement · cited by 735
- Filter.HasBasisstatement · cited by 604
- Metric.uniformity_basis_distproof · cited by 25
- nhds_basis_uniformityproof · cited by 21
Cited by41
Results whose statement or proof uses this declaration.
- Metric.mem_nhds_iffproof · cited by 26
- Metric.tendsto_nhdsproof · cited by 20
- Metric.mem_closure_iffproof · cited by 18
- Metric.tendsto_atTopproof · cited by 10
- Asymptotics.isLittleOTVS_iff_isLittleOproof · cited by 7
- Metric.tendsto_nhds_nhdsproof · cited by 6
- NormedSpace.isVonNBounded_of_isBoundedproof · cited by 4
- Metric.uniformity_eq_comap_nhds_zeroproof · cited by 4
- Asymptotics.isLittleOTVS_oneproof · cited by 4
- MeasureTheory.hasSum_integral_measureproof · cited by 4
- Real.dimH_of_mem_nhdsproof · cited by 3
- NormedAddGroup.nhds_basis_norm_ltproof · cited by 3