[Merged by Bors] - feat: sigma-compact sets#7576
Conversation
|
This PR/issue depends on:
|
079f039 to
2f7867a
Compare
|
@eric-wieser CI passes, so making the lemma you mentioned simp works. I presume Homeomorph.isCompact_image should also be a simp lemma then, and have PRed this as #7594. (I've also made the renames locally, but not checked all of mathlib yet; happy to drop those changes if need be. Update: CI passes, so presumably all is fine.) |
f44b5ef to
03d865e
Compare
Not checked other files yet; waiting for a naming decision from maintainers.
03d865e to
c52d65b
Compare
ADedecker
left a comment
There was a problem hiding this comment.
Thanks a lot, this looks very good already!
578b2a3 to
8080f7e
Compare
Co-authored-by: Oliver Nash <github@olivernash.org>
|
(Cancelling the build as this will need a rebase due to #7628 anyway.) |
ADedecker
left a comment
There was a problem hiding this comment.
Sorry for the wait! I think this is mostly good now, at most one more round.
e5df9ec to
da4a625
Compare
|
I have addressed all the comments, and also included some last touch-ups of related doc comments (in the last commit). |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thank you for the patient review. |
|
bors r+ |
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. - [x] depends on: #7528 Co-authored-by: David Loeffler <d.loeffler.01@cantab.net> Co-authored-by: grunweg <grunweg@posteo.de>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Define sigma-compact subsets of a topological space and show their basic properties.
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.
Similar to compact sets and spaces, we define sigma-compact subsets first, and relate sigma-compact spaces to them later.