Commit 2022-06-06 20:46 029a9551

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.