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(topology/locally_constant): Characteristic functions on clopen sets are locally constant #11708

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant #11708

wants to merge 19 commits into from

Conversation

laughinggas
Copy link
Collaborator

@laughinggas laughinggas commented Jan 28, 2022 •
edited by jcommelin
Loading

Gives an API for characteristic functions on clopen sets, char_fn, which are locally constant functions.

Open in Gitpod

@laughinggas laughinggas added the awaiting-review The author would like community review of the PR label Jan 28, 2022
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 31, 2022
@laughinggas laughinggas added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 31, 2022
@jcommelin
Copy link
Member

@laughinggas Note that there are linting errors: https://github.com/leanprover-community/mathlib/runs/5142642174?check_suite_focus=true
Please fix these.

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 12, 2022
jcommelin
jcommelin reviewed Mar 7, 2022
View reviewed changes
src/topology/locally_constant/algebra.lean Outdated Show resolved Hide resolved
src/topology/locally_constant/basic.lean Outdated Show resolved Hide resolved
@laughinggas laughinggas added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 10, 2022
@laughinggas laughinggas added awaiting-author A reviewer has asked the author a question or requested changes awaiting-review The author would like community review of the PR and removed awaiting-review The author would like community review of the PR awaiting-author A reviewer has asked the author a question or requested changes labels Mar 10, 2022
@jcommelin jcommelin removed the awaiting-review The author would like community review of the PR label Mar 11, 2022
@jcommelin jcommelin added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 16, 2022
@ocfnash ocfnash added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 29, 2022
@fpvandoorn
Copy link
Member

I merged your PR into master, and fixed the resulting errors in the file algebra/indicator_function (and simplified one proof).
I also reversed the directions of two iffs; could you make the same changes for your locally_constant versions of the lemmas?

@laughinggas
Copy link
Collaborator Author

Sorry for the late reply, I was travelling. I have made the changes, pls let me know if there is anything else I should do.

fpvandoorn
fpvandoorn reviewed May 13, 2022
View reviewed changes
Copy link
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

This PR is looking good now. I have a couple of minor comments about naming and similar, but after that I think we can merge it.

src/topology/locally_constant/algebra.lean Outdated Show resolved Hide resolved
src/topology/locally_constant/algebra.lean Outdated Show resolved Hide resolved
src/topology/locally_constant/algebra.lean Outdated Show resolved Hide resolved
src/topology/locally_constant/algebra.lean Outdated Show resolved Hide resolved
src/topology/locally_constant/algebra.lean Outdated Show resolved Hide resolved
@laughinggas
Copy link
Collaborator Author

All done, thanks a lot for the help!

@laughinggas laughinggas added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 19, 2022
@fpvandoorn
Copy link
Member

Thanks for bearing with us through all the changes! It looks good to me now.

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 19, 2022
bors bot pushed a commit that referenced this pull request May 19, 2022
@laughinggas @kbuzzard @fpvandoorn
feat(topology/locally_constant): Characteristic functions on clopen s…
ffe7002 
…ets are locally constant (#11708)

Gives an API for characteristic functions on clopen sets, `char_fn`, which are locally constant functions.



Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@bors
Copy link

bors bot commented May 19, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant [Merged by Bors] - feat(topology/locally_constant): Characteristic functions on clopen sets are locally constant May 19, 2022
@bors bors bot closed this May 19, 2022
@bors bors bot deleted the char_fn branch May 19, 2022 19:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin left review comments

@fpvandoorn fpvandoorn fpvandoorn left review comments

@ocfnash ocfnash ocfnash left review comments

@kbuzzard kbuzzard kbuzzard left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@laughinggas @jcommelin @fpvandoorn @eric-wieser @ocfnash @kbuzzard