mathlib3

35ef7700 - refactor(topology/compacts): Turn into structures, use `set_like`, cleanup (#12035)

refactor(topology/compacts): Turn into structures, use `set_like`, cleanup (#12035) * Change `closeds`, `compacts`, `nonempty_compacts`, `positive_compacts` from `subtype` to `structure` * Use `set_like` * Add missing instances * the `lattice` and `bounded_order` instances for `closeds` * the `bounded_order` instance for `compacts` * the `semilattice_sup` and `order_top` instances for `nonempty_compacts` * the `inhabited`, `semilattice_sup` and `order_top` instances for `positive_compacts` * kill `positive_compacts_univ` in favor of `⊤` using the new `order_top` instance * rename `nonempty_positive_compacts` to `positive_compacts.nonempty` * sectioning the file