mathlib
b6fa3beb - move(topology/sets/*): Move topological types of sets together (#12648)

Commit
3 years ago
move(topology/sets/*): Move topological types of sets together (#12648) Move * `topology.opens` to `topology.sets.opens` * `topology.compacts` to `topology.sets.closeds` and `topology.sets.compacts` `closeds` and `clopens` go into `topology.sets.closeds` and `compacts`, `nonempty_compacts`, `positive_compacts` and `compact_opens` go into `topology.sets.compacts`.
Author
Parents
Loading