mathlib3
67e0019b - refactor(topology/metric_space/baire): use choose! in Baire theorem (#3852)

Commit
5 years ago
refactor(topology/metric_space/baire): use choose! in Baire theorem (#3852) Use `choose!` in the proof of Baire theorem.
Author
Parents
Loading