feat(topology/metric_space/basic): dist_ne_zero (#7552)

leanprover-community · May 9, 2021 · bf229dd · bf229dd
1 parent 132328c
commit bf229dd
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
@@ -1755,6 +1755,9 @@ iff.intro eq_of_dist_eq_zero (assume : x = y, this ▸ dist_self _)
 @[simp] theorem zero_eq_dist {x y : γ} : 0 = dist x y ↔ x = y :=
 by rw [eq_comm, dist_eq_zero]
 
+theorem dist_ne_zero {x y : γ} : dist x y ≠ 0 ↔ x ≠ y :=
+by simpa only [not_iff_not] using dist_eq_zero
+
 @[simp] theorem dist_le_zero {x y : γ} : dist x y ≤ 0 ↔ x = y :=
 by simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y