Alexander sub-base theorem

Stream: Is there code for X?

[Christopher Hoskin]

Am I right in thinking that we don't currently have the Alexander sub-base theorem in Mathlib (if every cover by a sub-basis has a finite sub-cover then the space is compact)?

https://en.wikipedia.org/wiki/Subbase#Alexander_subbase_theorem