Pseudometric_Defines_an_Equivalence_Relation
Provedequivalence-relationsproofwikipseudometric-spacestopology
The relation x ~ y iff d(x,y) = 0 defined by a pseudometric is an equivalence relation.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Pseudometric_Defines_an_Equivalence_Relation {α : Type _} [PseudoMetricSpace α] : Equivalence (fun x y : α => dist x y = 0) := by sorrySource