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_finite): add lemmas about option _ and sum _ _ #15923

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(topology/locally_finite): add lemmas about option _ and sum _ _ #15923

wants to merge 8 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Aug 7, 2022

Open in Gitpod

@urkud urkud added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Aug 7, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Aug 8, 2022
eric-wieser
eric-wieser reviewed Aug 8, 2022
View reviewed changes
src/data/set/finite.lean
@@ -594,6 +594,11 @@ theorem finite_mem_finset (s : finset α) : {a | a ∈ s}.finite := to_finite _
lemma subsingleton.finite {s : set α} (h : s.subsingleton) : s.finite :=
h.induction_on finite_empty finite_singleton

lemma finite_preimage_inl_and_inr {s : set (α ⊕ β)} :
(sum.inl ⁻¹' s).finite ∧ (sum.inr ⁻¹' s).finite ↔ s.finite :=
Copy link
Member

Choose a reason for hiding this comment

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

Do you think this should be called finite_sum instead, to match locally_finite_sum below?

Also, do we have the option version already?

Copy link
Member Author

Choose a reason for hiding this comment

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

Then we should swap LHS with RHS. I'm not sure that we have an established naming (or LHS/RHS) convention for this kind of lemmas. I can start a topic on Zulip after ITP.

Copy link
Member

Choose a reason for hiding this comment

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

Sorry, I meant to include "swap sides" in that comment.

Copy link
Member

Choose a reason for hiding this comment

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

What is the status here?

Copy link
Member Author

Choose a reason for hiding this comment

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

I've got covid and didn't start the discussion on Zulip.

@urkud @eric-wieser
Update src/topology/locally_finite.lean
4e5230d 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jcommelin
jcommelin approved these changes Sep 2, 2022
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.

LGTM, but there is an ongoing discussion.

src/data/set/finite.lean
@@ -594,6 +594,11 @@ theorem finite_mem_finset (s : finset α) : {a | a ∈ s}.finite := to_finite _
lemma subsingleton.finite {s : set α} (h : s.subsingleton) : s.finite :=
h.induction_on finite_empty finite_singleton

lemma finite_preimage_inl_and_inr {s : set (α ⊕ β)} :
(sum.inl ⁻¹' s).finite ∧ (sum.inr ⁻¹' s).finite ↔ s.finite :=
Copy link
Member

Choose a reason for hiding this comment

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

What is the status here?

@j-loreaux
Copy link
Collaborator

I'm not sure that we have an established naming (or LHS/RHS) convention for this kind of lemmas. I can start a topic on Zulip after ITP.

There was a discussion that was supposed to take place on Zulip, but it appears it never happened. While it is slightly related to the PR, I don't think it's necessary to keep it on the queue for this reason, especially since the discussion never started.

maintainer merge

@j-loreaux
Copy link
Collaborator

maintainer merge

@j-loreaux j-loreaux self-assigned this Oct 5, 2022
jcommelin
jcommelin approved these changes Oct 5, 2022
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

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Oct 5, 2022
@j-loreaux
Copy link
Collaborator

maintainer merge

@github-actions
Copy link

github-actions bot commented Oct 5, 2022

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

bors bot pushed a commit that referenced this pull request Oct 5, 2022
@urkud @j-loreaux
feat(topology/locally_finite): add lemmas about option _ and `sum _…
7952bc6 
… _` (#15923)




Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@bors
Copy link

bors bot commented Oct 6, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/locally_finite): add lemmas about option _ and sum _ _ [Merged by Bors] - feat(topology/locally_finite): add lemmas about option _ and sum _ _ Oct 6, 2022
@bors bors bot closed this Oct 6, 2022
@bors bors bot deleted the YK-loc-fin-option branch October 6, 2022 00:19
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 approved these changes

Assignees

@j-loreaux j-loreaux

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) 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
5 participants
@urkud @j-loreaux @eric-wieser @jcommelin @leanprover-community-bot-assistant