∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : EMetricSpace β] {K : NNReal} {f : α → β}
  [CompleteSpace α], AntilipschitzWith K f → UniformContinuous f → Topology.IsClosedEmbedding f