mathlib

8770f5c7 - refactor(topology/subset_properties): more properties of `compact_covering` (#6328)

refactor(topology/subset_properties): more properties of `compact_covering` (#6328) Modify the definition of `compact_covering α n` to ensure that it is monotone in `n`. Also, in a locally compact space, prove the existence of a compact exhaustion, i.e. a sequence which satisfies the properties for `compact_covering` and in which, moreover, the interior of the next set includes the previous set.