Zulip Chat Archive

Stream: Is there code for X?

Topic: is this lemma true?


view this post on Zulip Jesse Michael Han (Nov 30 2020 at 21:00):

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

view this post on Zulip Alex J. Best (Nov 30 2020 at 21:16):

is docs#uniform_embedding.dense_embedding what you want?

view this post on Zulip Alex J. Best (Nov 30 2020 at 21:17):

Looks like it needs dense range too

view this post on Zulip Patrick Massot (Nov 30 2020 at 21:33):

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


Last updated: May 07 2021 at 23:11 UTC