Theorems · Theorem · general topology
uniformContinuous_dist
∀ {α : Type u_1} [inst : PseudoMetricSpace α], UniformContinuous fun p => dist p.1 p.2- Cited by
- 4 results in Mathlib
- Foundations
- Depth 152 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.
Cites12
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
- PseudoMetricSpacestatement and proof · cited by 1,550
- Dist.diststatement and proof · cited by 1,539
- add_le_addproof · cited by 666
- UniformContinuousstatement · cited by 410
- le_max_leftproof · cited by 215
- le_max_rightproof · cited by 205
- half_posproof · cited by 83
- add_halvesproof · cited by 78
- add_lt_addproof · cited by 35
- Metric.uniformContinuous_iffproof · cited by 13
- dist_dist_dist_leproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- UniformSpace.Completion.dist_eqproof · cited by 10
- continuous_distproof · cited by 9
- uniformContinuous_nndistproof · cited by 2
- UniformContinuous.distproof · cited by 0