Theorems · Theorem · general topology
dist_eq_zero
∀ {γ : Type w} [inst : MetricSpace γ] {x y : γ}, dist x y = 0 ↔ x = y- Defined in
- Mathlib.Topology.MetricSpace.Defs
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MetricSpace
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.
- Realstatement · cited by 25,697
- MetricSpacestatement and proof · cited by 1,684
- Dist.diststatement · cited by 1,539
- dist_selfproof · cited by 116
- eq_of_dist_eq_zeroproof · cited by 2
Cited by13
Results whose statement or proof uses this declaration.
- dist_ne_zeroproof · cited by 13
- dist_le_zeroproof · cited by 7
- Metric.sphere_zeroproof · cited by 5
- EuclideanGeometry.dist_orthogonalProjection_eq_dist_iff_eq_of_memproof · cited by 2
- EuclideanGeometry.dist_orthogonalProjection_eq_zero_iffproof · cited by 2
- EuclideanGeometry.left_dist_ne_zero_of_angle_eq_piproof · cited by 2
- EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mulproof · cited by 1
- EuclideanGeometry.Sphere.IsDiameter.left_eq_right_iffproof · cited by 1
- Similar.angle_eqproof · cited by 1
- Affine.Simplex.Equilateral.angle_eq_pi_div_threeproof · cited by 1
- EuclideanGeometry.Sphere.isIntTangent_iff_dist_centerproof · cited by 0