Mathlib v3 is deprecated. Go to Mathlib v4

Def topological_space.nonempty_compacts.to_closeds

Modification history

2022-10-13 15:02
src/topology/sets/compacts.lean
refactor(topology/sets/compacts): rename projection to is_compact (#16949) …
Modified topological_space.nonempty_compacts.to_closedsView on Github →
2022-02-22 18:15
src/topology/compacts.lean
refactor(topology/compacts): Turn into structures, use `set_like`, cleanup (#12035) …
Modified topological_space.nonempty_compacts.to_closedsView on Github →
2020-07-06 07:16
src/topology/compacts.lean
feat(topology): preliminaries for Haar measure (#3194) …
Modified topological_space.nonempty_compacts.to_closedsView on Github →
2020-02-23 17:01
src/topology/opens.lean
feat(topology): an `is_complete` set is a `complete_space` (#2037) …
Modified topological_space.nonempty_compacts.to_closedsView on Github →
2019-03-03 19:05
src/topology/opens.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Added topological_space.nonempty_compacts.to_closedsView on Github →