mathlib3

feat(topology/metric_space/baire): Baire theorem

#816

Merged