Skip to content

Restricted products (wrt opens) commute with finite products #570

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.

Sign up for GitHub

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

Jump to bottom
Closed
kbuzzard opened this issue May 29, 2025 · 2 comments · Fixed by #594
Closed

Restricted products (wrt opens) commute with finite products #570

kbuzzard opened this issue May 29, 2025 · 2 comments · Fixed by #594
Assignees
@b-mehta

Comments

@kbuzzard
Copy link
Collaborator

The claim is that restricted products commute with finite products. This is vacuous if the product is empty and it's Homeomorph.restrictedProductProd for a binary product, so now it should be mathematically straightforward to deduce it for finite products. The blueprint just says "induction on the size of the finite set". The declaration is Homeomorph.restrictedProductPi in FLT/Mathlib/Topology/Algebra/RestrictedProduct.lean.
@kbuzzard kbuzzard added WIP and removed WIP labels May 29, 2025
@github-project-automation github-project-automation bot moved this to Unclaimed in FLT Project May 31, 2025
@b-mehta
Copy link
Contributor

b-mehta commented Jun 1, 2025

claim

@kbuzzard kbuzzard moved this from Unclaimed to Claimed in FLT Project Jun 1, 2025
@b-mehta
Copy link
Contributor

b-mehta commented Jun 1, 2025

propose #594

@github-actions github-actions bot mentioned this issue Jun 1, 2025
Merged
@kbuzzard kbuzzard moved this from Claimed to In Progress in FLT Project Jun 1, 2025
@kbuzzard kbuzzard moved this from In Progress to In Review in FLT Project Jun 1, 2025
@github-project-automation github-project-automation bot moved this from In Review to Completed in FLT Project Jun 1, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@b-mehta b-mehta

Labels
None yet
Projects
FLT Project
Status: Completed
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat: restricted products and finite products b-mehta/FLT
2 participants
@b-mehta @kbuzzard