Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_positive_compacts_subset

Modification history

2022-06-06 20:46
src/topology/sets/compacts.lean
refactor(../metric_space/baire): add baire_space class and instances (#14547) …
Added exists_positive_compacts_subsetView on Github →