is this lemma true?

Stream: Is there code for X?

[Jesse Michael Han]

example {α β : Type u} [uniform_space α] [uniform_space β] {f : α → β}
  : uniform_inducing f → function.injective f → dense_embedding f
:= sorry

[Alex J. Best]

is docs#uniform_embedding.dense_embedding what you want?

[Alex J. Best]

Looks like it needs dense range too

[Patrick Massot]

I don't see how you could get a dense range for free.