[Merged by Bors] - feat: analogue of iSup.prod for sets#7528
[Merged by Bors] - feat: analogue of iSup.prod for sets#7528
Conversation
599e4c7 to
d41c960
Compare
Mathlib/Data/Set/Lattice.lean
Outdated
|
|
||
| /-- Analogue of `iSup.prod` for sets. -/ | ||
| lemma Set.iUnion_prod' {X Y Z : Type*} (f : X × Y → Set Z) : | ||
| ⋃ (x : X) (y : Y), (f ⟨x, y⟩) = ⋃ t : X × Y, (f t) := by |
There was a problem hiding this comment.
Could you put the statement in the same order as iSup_prod? Ideally the proof would be precisely iSup_prod.
There was a problem hiding this comment.
I have reversed the statement (and renamed all variables to exactly match iSup_prod. The proof becomes one line longer, though.
|
(Guessing a topic in the sense of mathlib.) |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Anatole Dedecker.
|
Thank you for the fast review. |
|
bors r+ |
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. * 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>
As suggested on Zulip.
Feedback on the lemma name is appreciated;
iUnion_prodis already taken by a different lemma.