Mathlib v3 is deprecated. Go to Mathlib v4

Def nonempty_compacts.to_closeds

Modification history

2019-03-03 19:05
src/topology/constructions.lean
chore(topology): Splits topology.basic and topology.continuity (#785) …
Deleted nonempty_compacts.to_closedsView on Github →
2019-03-01 22:25
src/topology/continuity.lean
feat(topology/metric_space/hausdorff_distance): Hausdorff distance
Added nonempty_compacts.to_closedsView on Github →