theorem Metric.IsSeparated.zero {X : Type u_3} [EMetricSpace X] (s : Set X) : IsSeparated 0 s

Alias of Metric.isSeparated_zero.

theorem AntilipschitzWith.injOn {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s : Set X} {K ε : NNReal} (hf : AntilipschitzWith K f) (hs : Metric.IsSeparated (↑ε) s) : Set.InjOn f s

theorem Metric.IsSeparated.image_of_antilipschitzWith {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {f : X → Y} {s : Set X} {K ε : NNReal} (hf : AntilipschitzWith K f) (hs : IsSeparated (↑K * ↑ε) s) : IsSeparated (↑ε) (f '' s)