-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(topology/subset_properties): locally_compact_space
instance for Π
types
#15707
Conversation
I just pushed a version without the compact assumption in the finite case, which is a generalization of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for this!
I think it is worth turning the PR comment about cofinitely-many compact spaces "In general it suffices that all but finitely many of the spaces are compact, but that's not straightforward to state and use." into a code comment.
Please also apply the other suggestions and then feel free to merge.
bors d+
✌️ ralvrz can now approve this pull request. To approve and merge a pull request, simply reply with |
bors d=alreadydone |
✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <github@olivernash.org>
bors r+ |
…r `Π` types (#15707) This PR adds - `locally_compact_space.pi` mirroring `locally_compact_space.prod` and - `locally_compact_space.pi_finite` for finite products Proof by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Pull request successfully merged into master. Build succeeded: |
locally_compact_space
instance for Π
typeslocally_compact_space
instance for Π
types
…r `Π` types (leanprover-community#15707) This PR adds - `locally_compact_space.pi` mirroring `locally_compact_space.prod` and - `locally_compact_space.pi_finite` for finite products Proof by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
…r `Π` types (#15707) This PR adds - `locally_compact_space.pi` mirroring `locally_compact_space.prod` and - `locally_compact_space.pi_finite` for finite products Proof by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
…r `Π` types (#15707) This PR adds - `locally_compact_space.pi` mirroring `locally_compact_space.prod` and - `locally_compact_space.pi_finite` for finite products Proof by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
…r `Π` types (#15707) This PR adds - `locally_compact_space.pi` mirroring `locally_compact_space.prod` and - `locally_compact_space.pi_finite` for finite products Proof by: @alreadydone Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
This PR adds
locally_compact_space.pi
mirroringlocally_compact_space.prod
andlocally_compact_space.pi_finite
for finite productsProof by: @alreadydone