mathlib

029a9551 - refactor(../metric_space/baire): add baire_space class and instances (#14547)

refactor(../metric_space/baire): add baire_space class and instances (#14547) * Add a `baire_space` class containing the Baire property (a countable intersection of open dense sets is dense). * The Baire category theorem for complete metric spaces becomes an instance of `baire_space`. * Previous consequences of the Baire property use `baire_space` as an hypothesis, instead of `pseudo_emetric_space` `complete_space`. * Add an instance of `baire_space` for locally compact t2 spaces, in effect extending all the consequences of the Baire property to locally compact spaces. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>