Theorems · Theorem · general topology
edist_eq_zero
∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, edist x y = 0 ↔ x = yCharacterize the equality of points by the vanishing of their extended distance
- Defined in
- Mathlib.Topology.EMetricSpace.Defs
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- EMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- EDist.ediststatement · cited by 735
- EMetricSpacestatement and proof · cited by 242
- PseudoEMetricSpace.edist_selfproof · cited by 50
- EMetricSpace.eq_of_edist_eq_zeroproof · cited by 2
Cited by4
Results whose statement or proof uses this declaration.
- edist_le_zeroproof · cited by 3
- eHolderNorm_eq_zeroproof · cited by 1
- zero_eq_edistproof · cited by 0
- Dilation.ratio_compproof · cited by 0