Commit 2023-10-16 22:36 eece5add

feat: sigma-compact sets (#7576) Define sigma-compact subsets of a topological space and show their basic properties.

• compact sets are sigma-compact
• countable unions of (sigma-)compact sets are sigma-compact
• closed subsets of sigma-compact sets are sigma-compact. Relate them to sigma-compact space: a set is sigma-compact iff it is a sigma-compact space (w.r.t. the subspace topology). In a later PR, we'll show that sigma-compact measure zero sets are nowhere dense.

• depends on: #7528