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: port Topology.ContinuousFunction.ZeroAtInfty #4255

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat: port Topology.ContinuousFunction.ZeroAtInfty #4255

wants to merge 10 commits into from

Conversation

int-y1
Copy link
Collaborator

@int-y1 int-y1 commented May 23, 2023 •
edited by j-loreaux

Open in Gitpod

@int-y1 int-y1 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. awaiting-review The author would like community review of the PR awaiting-CI help-wanted The author needs attention to resolve issues and removed WIP Work in progress awaiting-review The author would like community review of the PR awaiting-CI labels May 23, 2023
@eric-wieser eric-wieser force-pushed the port/Topology.ContinuousFunction.ZeroAtInfty branch from 6a4443c to 21416cd Compare May 24, 2023 15:40
@eric-wieser
Copy link
Member

I did a rebase on top of the latest mathport output. Please do git reset --hard origin/port/Topology.ContinuousFunction.ZeroAtInfty next time you work on this branch.

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 5, 2023
@j-loreaux j-loreaux force-pushed the port/Topology.ContinuousFunction.ZeroAtInfty branch from 0352339 to 6ac1c8b Compare June 6, 2023 20:59
@j-loreaux j-loreaux added awaiting-review The author would like community review of the PR and removed help-wanted The author needs attention to resolve issues merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Jun 6, 2023
@ChrisHughes24
Copy link
Member

I don't understand why the linter fails in files that do not have dependencies touched by this PR.

@j-loreaux
Copy link
Collaborator

j-loreaux commented Jun 16, 2023 •
edited

We'll see what CI says, but I think the issue was an @[simps] in a place where it shouldn't exist that was generating a stupid lemma of the form [ContinuousMapClass F] [CompactSpace X] (f : F) (x : X) : f x = f x (possibly with different instances on the right and left-hand sides of this, I didn't check). Then whenever Lean had a ContinuousMapClass instance and something that looked like f x it went on a hunt for a CompactSpace instance on the domain. I think just deleting the @[simps] is the solution.

jcommelin
jcommelin approved these changes Jun 16, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@semorrison semorrison 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 Jun 16, 2023
bors bot pushed a commit that referenced this pull request Jun 16, 2023
@eric-wieser @int-y1
@j-loreaux @ChrisHughes24
feat: port Topology.ContinuousFunction.ZeroAtInfty (#4255)
b21a13b 
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
@bors
Copy link

bors bot commented Jun 16, 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: port Topology.ContinuousFunction.ZeroAtInfty [Merged by Bors] - feat: port Topology.ContinuousFunction.ZeroAtInfty Jun 16, 2023
@bors bors bot closed this Jun 16, 2023
@bors bors bot deleted the port/Topology.ContinuousFunction.ZeroAtInfty branch June 16, 2023 17:43
jcommelin pushed a commit that referenced this pull request Jun 17, 2023
@eric-wieser @int-y1
@j-loreaux @ChrisHughes24 @jcommelin
feat: port Topology.ContinuousFunction.ZeroAtInfty (#4255)
93dcedf 
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
alexkeizer pushed a commit that referenced this pull request Jun 22, 2023
@eric-wieser @int-y1
@j-loreaux @ChrisHughes24 @alexkeizer
feat: port Topology.ContinuousFunction.ZeroAtInfty (#4255)
824715f 
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
semorrison pushed a commit that referenced this pull request Jun 23, 2023
@eric-wieser @int-y1
@j-loreaux @ChrisHughes24 @semorrison
feat: port Topology.ContinuousFunction.ZeroAtInfty (#4255)
52b08f6 
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
semorrison pushed a commit that referenced this pull request Jun 25, 2023
@eric-wieser @int-y1
@j-loreaux @ChrisHughes24 @semorrison
feat: port Topology.ContinuousFunction.ZeroAtInfty (#4255)
ce71be8 
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@int-y1 @eric-wieser @ChrisHughes24 @j-loreaux @jcommelin @semorrison @fpvandoorn