Theorems · Theorem · general topology
edist_nndist
∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y = ↑(nndist x y)Express edist in terms of nndist
- Defined in
- Mathlib.Topology.MetricSpace.Pseudo.Defs
- Cited by
- 38 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.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- ENNRealstatement and proof · cited by 9,879
- PseudoMetricSpacestatement and proof · cited by 1,550
- ENNReal.ofNNRealstatement and proof · cited by 1,279
- ENNReal.ofRealproof · cited by 863
- EDist.ediststatement · cited by 735
- NNDist.nndiststatement and proof · cited by 235
- ENNReal.ofReal_coe_nnrealproof · cited by 52
- edist_distproof · cited by 39
- dist_nndistproof · cited by 10
Cited by38
Results whose statement or proof uses this declaration.
- edist_zero_rightproof · cited by 25
- lipschitzWith_iff_dist_le_mulproof · cited by 10
- coe_nnreal_ennreal_nndistproof · cited by 4
- Metric.inseparable_iff_nndistproof · cited by 3
- edist_smul₀proof · cited by 3
- HolderOnWith.nndist_le_of_leproof · cited by 3
- BoundedContinuousFunction.edist_eq_iSupproof · cited by 3
- lipschitzOnWith_iff_dist_le_mulproof · cited by 3
- congruent_iff_nndist_eqproof · cited by 3
- similar_iff_exists_nndist_eqproof · cited by 3
- antilipschitzWith_iff_le_mul_nndistproof · cited by 2
- PiLp.edist_single_sameproof · cited by 2