Skip to content
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

[Merged by Bors] - feat: open maps from I × X, I discrete #7809

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat: open maps from I × X, I discrete #7809

wants to merge 2 commits into from

Conversation

ADedecker
Copy link
Member

Open in Gitpod

@ADedecker ADedecker added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 20, 2023
@ADedecker ADedecker mentioned this pull request Oct 20, 2023
Open
@digama0
Copy link
Member

digama0 commented Oct 21, 2023

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

alreadydone
alreadydone approved these changes Oct 23, 2023
View reviewed changes
Copy link
Contributor

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, but I'm not sure the lemmas can be applied where you intended them to (see comment).

@sgouezel
Copy link
Contributor

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Oct 30, 2023
bors bot pushed a commit that referenced this pull request Oct 30, 2023
@ADedecker @digama0
feat: open maps from I × X, I discrete (#7809)
2d628e7 
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@bors
Copy link

bors bot commented Oct 30, 2023

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.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: open maps from I × X, I discrete [Merged by Bors] - feat: open maps from I × X, I discrete Oct 30, 2023
@bors bors bot closed this Oct 30, 2023
@bors bors bot deleted the AD_open_map_misc branch October 30, 2023 12:16
grunweg pushed a commit that referenced this pull request Nov 1, 2023
@ADedecker @digama0 @grunweg
feat: open maps from I × X, I discrete (#7809)
8671b30 
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
fgdorais pushed a commit that referenced this pull request Nov 1, 2023
@ADedecker @digama0 @fgdorais
feat: open maps from I × X, I discrete (#7809)
c5b50df 
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone approved these changes

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@ADedecker @digama0 @sgouezel @alreadydone