Where to put theorem about separable metric spaces

Stream: mathlib4

[Luigi Massacci]

Hello,

I found myself needing this simple theorem, which is not in Mathlib:

theorem Embedding.separableMetricSpace {α : Type u_1} {β : Type u_2} [MetricSpace α]
  [MetricSpace β] {f : α → β} [TopologicalSpace.SeparableSpace β]
    (hf : Embedding f) : TopologicalSpace.SeparableSpace α := by
    have := UniformSpace.secondCountable_of_separable β
    have := Embedding.secondCountableTopology hf
    exact TopologicalSpace.SecondCountableTopology.to_separableSpace

(I guess the most general case where this is true might be a first countable topological space, or something like that, but that would be more painful to prove and I needed it only for metric spaces)

Under the possibly mistaken assumption that this does belong in Mathlib, I'm somewhat at a loss as to where it should go.

[Ruben Van de Velde]

import Mathlib
theorem Embedding.separableMetricSpace {α : Type u_1} {β : Type u_2} [MetricSpace α]
  [MetricSpace β] {f : α → β} [TopologicalSpace.SeparableSpace β]
    (hf : Embedding f) : TopologicalSpace.SeparableSpace α := by
    have := UniformSpace.secondCountable_of_separable β
    have := Embedding.secondCountableTopology hf
    exact TopologicalSpace.SecondCountableTopology.to_separableSpace
#find_home Embedding.separableMetricSpace -- [Mathlib.Topology.MetricSpace.Basic]

seems plausible

[Luigi Massacci]

Thank you! I did not know about find_home, that is magic. I did think about MetricSpace.Basic, but the thing is that the stuff there really is very basic; still, it's not implausible, I'll PR it and we'll see...

[Jireh Loreaux]

First-countability is not enough to guarantee that subsets of separable spaces are separable. In particular, the Sorgenfrey plane is a counterexample. But you should be able to reduce this to assuming only second-countability.

[Luigi Massacci]

You mean something like this?

theorem Embedding.separableMetricSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α]
  [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : Embedding f) :
    TopologicalSpace.SeparableSpace α := by
  have := Embedding.secondCountableTopology hf
  exact TopologicalSpace.SecondCountableTopology.to_separableSpace

it feels a bit forced

[Jireh Loreaux]

Why more so than the one you have above? It's the same argument.

[Jireh Loreaux]

Probably the #find_home for that will make a bit more sense.

[Jireh Loreaux]

And note that in your original version there's no need to assume α is a metric space anyway.

[Luigi Massacci]

Because you have second countable on one side and separable on the other.

[Jireh Loreaux]

Yeah, but you have to have something like this, because separability is not hereditary.