Commit 2021-02-25 21:38 8770f5c7

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.