CompactSpace + MetricSpace gives SeparableSpace

Stream: Is there code for X?

[Josha Dekker]

Do we have that a compact metric space is separable? I just came across the statement in a textbook I'm reading (I forgot about it) and I didn't recall proving the analogous result for Lindelöf spaces when I added the basic API for Lindelöf spaces, so thought I'd quickly modify the proof to work for Lindelöf and deduce compact/sigma-compact from there.

[Sébastien Gouëzel]

variable {α : Type*} [MetricSpace α] [CompactSpace α]
#synth TopologicalSpace.SeparableSpace α

succeeds. So the answer is yes, we have it. And #synth will even tell you how it got there.

[Josha Dekker]

Thank you, I tried moogle and loogle, but I wasn’t successful there… I didn’t think of this way!

[Notification Bot]

Josha Dekker has marked this topic as resolved.

[Sébastien Gouëzel]

It's gonna be pretty indirect, unless you use the minimal classes, so #synth is really your best friend here. (It will go through second countable topology, and proper spaces...)

[Sébastien Gouëzel]

Note that our library is not optimal:

variable {α : Type*} [TopologicalSpace α] [TopologicalSpace.MetrizableSpace α] [CompactSpace α]
#synth SecondCountableTopology α

fails.

[Anatole Dedecker]

Yes, I think there are a lot of things that never moved to MetrizableSpace when it was introduced.

[Josha Dekker]

I’ll write up that metric (metrizable?) Lindelöf spaces are second countable. If I’ve got time I’ll do it tomorrow, I’m not very familiar with the metric spaces part of the topology library, so not sure how quickly I’ll get it done.

[Notification Bot]

Josha Dekker has marked this topic as unresolved.

[Josha Dekker]

In the small PR #10376 I add that a Pseudometric Lindelöf space is a SecondCountableTopology, from which SeparableSpace can be synthesised.

[Josha Dekker]

Sébastien Gouëzel said:

Note that our library is not optimal:

variable {α : Type*} [TopologicalSpace α] [TopologicalSpace.MetrizableSpace α] [CompactSpace α]
#synth SecondCountableTopology α

fails.

I've incorporated your suggestion on #10376, now this instance also works (via CompactSpace -> LindelofSpace and Metrizable -> PseudoMetrizable)) (after dropping [TopologicalSpace α])