Theorems · Theorem · general topology
Metric.uniformity_basis_dist
∀ {α : Type u} [inst : PseudoMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | dist p.1 p.2 < ε}- Defined in
- Mathlib.Topology.MetricSpace.Pseudo.Defs
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 113 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.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Set.ofPredstatement and proof · cited by 6,101
- UniformSpaceproof · cited by 2,040
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement and proof · cited by 1,539
- uniformitystatement and proof · cited by 765
- Filter.HasBasisstatement and proof · cited by 604
- dist_commproof · cited by 188
- dist_selfproof · cited by 116
- NoMaxOrder.exists_gtproof · cited by 62
- dist_triangleproof · cited by 44
- UniformSpace.hasBasis_ofFunproof · cited by 3
Cited by25
Results whose statement or proof uses this declaration.
- Metric.nhds_basis_ballproof · cited by 41
- Metric.uniformContinuous_iffproof · cited by 13
- Metric.cauchySeq_iff'proof · cited by 8
- Metric.mem_uniformity_distproof · cited by 8
- Metric.mk_uniformity_basisproof · cited by 7
- Metric.totallyBounded_iffproof · cited by 5
- Metric.cauchySeq_iffproof · cited by 4
- Metric.mk_uniformity_basis_leproof · cited by 4
- Metric.cauchy_iffproof · cited by 3
- lebesgue_number_lemma_of_metricproof · cited by 3
- Metric.isUniformInducing_iffproof · cited by 3