Metric-separated sets

In this section we define the predicate Metric.IsSeparated' for ε-separated sets.

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

A set s is ≥ ε-separated if its elements are pairwise at distance greater or equal to ε from each other.

Equations

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