TODO

Rename IsMetricSeparated to Metric.AreSeparated

def Metric.IsSeparated {X : Type u_1} [EMetricSpace X] (ε : ENNReal) (s : Set X) : Prop

Equations

• Metric.IsSeparated ε s = s.Pairwise fun (x1 x2 : X) => ε ≤ edist x1 x2