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: partition into subintervals/squares adapted to an open cover #7915

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat: partition into subintervals/squares adapted to an open cover #7915

wants to merge 19 commits into from

Conversation

alreadydone
Copy link
Contributor

@alreadydone alreadydone commented Oct 25, 2023 •
edited by eric-wieser

Also adds some useful instances and lemmas about the unit interval.

The subsquares version will be useful for Van Kampen.

Open in Gitpod

@alreadydone alreadydone added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 25, 2023
@alreadydone alreadydone added WIP Work in progress 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 Oct 27, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Oct 27, 2023
@alreadydone alreadydone force-pushed the UnitInterval_LebesgueNumberLemma branch from 86c9650 to c09aad2 Compare October 27, 2023 20:29
@alreadydone alreadydone changed the title feat: partition into subintervals adapted to an open cover feat: partition into subintervals/squares adapted to an open cover Oct 28, 2023
@alreadydone alreadydone force-pushed the UnitInterval_LebesgueNumberLemma branch from c09aad2 to ce2deef Compare October 28, 2023 04:34
@alreadydone alreadydone added awaiting-review The author would like community review of the PR awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes WIP Work in progress labels Oct 28, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Oct 30, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

alreadydone
alreadydone commented Nov 9, 2023
View reviewed changes
Copy link
Contributor Author

@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.

Thanks for the review!

Mathlib/Topology/UnitInterval.lean Show resolved Hide resolved
Mathlib/Topology/UnitInterval.lean Show resolved Hide resolved
Mathlib/Topology/UnitInterval.lean Outdated Show resolved Hide resolved
Mathlib/Topology/UnitInterval.lean Outdated Show resolved Hide resolved
Mathlib/Topology/UnitInterval.lean Outdated Show resolved Hide resolved
Mathlib/Topology/UnitInterval.lean Outdated Show resolved Hide resolved
@alreadydone @eric-wieser
docstring
27064e4 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@eric-wieser eric-wieser removed their request for review November 10, 2023 13:59
@eric-wieser
Copy link
Member

None of my comments above are intended to be blocking, this is outside an area I'm all that familiar with; they were intended as discussion points for (or to be ignored by) another reviewer who knows better.

@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 Nov 10, 2023
@alreadydone alreadydone 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 Nov 10, 2023
PatrickMassot
PatrickMassot reviewed Nov 28, 2023
View reviewed changes
Copy link
Member

@PatrickMassot PatrickMassot left a comment

Choose a reason for hiding this comment

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

bors d+

Mathlib/Topology/UnitInterval.lean Outdated Show resolved Hide resolved
Mathlib/Topology/UnitInterval.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link

mathlib-bors bot commented Nov 28, 2023

✌️ alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Nov 28, 2023
@alreadydone
Copy link
Contributor Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Nov 30, 2023
@alreadydone
feat: partition into subintervals/squares adapted to an open cover (#…
392482f 
…7915)

Also adds some useful instances and lemmas about the unit interval.

The subsquares version will be useful for Van Kampen.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Nov 30, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: partition into subintervals/squares adapted to an open cover [Merged by Bors] - feat: partition into subintervals/squares adapted to an open cover Nov 30, 2023
@mathlib-bors mathlib-bors bot closed this Nov 30, 2023
@mathlib-bors mathlib-bors bot deleted the UnitInterval_LebesgueNumberLemma branch November 30, 2023 16:05
awueth pushed a commit that referenced this pull request Dec 19, 2023
@alreadydone @awueth
feat: partition into subintervals/squares adapted to an open cover (#…
288c64d 
…7915)

Also adds some useful instances and lemmas about the unit interval.

The subsquares version will be useful for Van Kampen.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

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

@PatrickMassot PatrickMassot PatrickMassot left review comments

Assignees
No one assigned
Labels
delegated t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
Covering spaces and étale spaces
Status: Merged
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@alreadydone @leanprover-community-mathlib4-bot @eric-wieser @urkud @PatrickMassot @jcommelin