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/paracompact): define paracompact spaces #6395

Closed
wants to merge 49 commits into from
Closed

[Merged by Bors] - feat(topology/paracompact): define paracompact spaces #6395

wants to merge 49 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Feb 24, 2021 •
edited by github-actions bot

urkud and others added 16 commits February 20, 2021 12:52
@urkud
chore(topology/bases): golf a proof
a4ecf9d 
Also add some supporting lemmas
@urkud
Snapshot
d98fd1a
@urkud
Merge branch 'master' into compact-covering
926394e
@urkud
chore(topology): move exists_compact_superset, drop assumption `t2_…
19fd725 
…space`

Also golf the proof of `is_compact.elim_finite_subcover_image`
@urkud
Merge branch 'compact-superset' into compact-covering
4a1c1a9
@urkud
Snapshot
2d45baa
@urkud
Merge branch 'master' into compact-covering
db1efd6
@urkud
Snapshot
f80960b
@urkud
Merge branch 'compact-covering' into paracompact
6f3393c
@urkud
Snapshot
84a5ad8
@urkud
Merge branch 'master' into compact-covering
2d868dc
@urkud
Modify as requested
b227e76
@urkud
Merge branch 'compact-covering' into paracompact
e6086d0
@urkud @hrmacbeth
Apply suggestions from code review
2487982 
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
@urkud
Snapshot
c395407
@urkud
Fix
3e8be4c
@urkud urkud added the WIP Work in progress label Feb 24, 2021
@urkud urkud added this to In progress in Partition of unity via automation Feb 24, 2021
@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 24, 2021
@urkud urkud changed the title feat(topology/paracompact): defie paracompact spaces feat(topology/paracompact): define paracompact spaces Feb 24, 2021
@urkud urkud mentioned this pull request Feb 24, 2021
Closed
2 tasks
@github-actions
Copy link

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

sgouezel
sgouezel reviewed Mar 2, 2021
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

I'm asking for more documentation, as usual :-)

src/topology/paracompact.lean Outdated Show resolved Hide resolved
src/topology/metric_space/emetric_space.lean Show resolved Hide resolved
@urkud
Copy link
Member Author

urkud commented Mar 3, 2021

I added quite a few comments and refactored the definition to use indexed coverings both in "if" and "then" parts.

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 4, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 4, 2021
@urkud @jcommelin
Update src/topology/paracompact.lean
cd4f1e5 
Co-authored-by: Johan Commelin <johan@commelin.net>
urkud
urkud commented Mar 4, 2021
View reviewed changes
src/topology/paracompact.lean Outdated Show resolved Hide resolved
Partition of unity automation moved this from In progress to Reviewer approved Mar 4, 2021
sgouezel
sgouezel reviewed Mar 5, 2021
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

Thanks a lot for improving the docs!

src/topology/metric_space/emetric_space.lean Outdated Show resolved Hide resolved
src/topology/paracompact.lean Outdated Show resolved Hide resolved
src/topology/paracompact.lean Outdated Show resolved Hide resolved
src/topology/paracompact.lean Outdated Show resolved Hide resolved
@sgouezel
Copy link
Collaborator

sgouezel commented Mar 6, 2021

bors r+
Thanks!

@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 Mar 6, 2021
bors bot pushed a commit that referenced this pull request Mar 6, 2021
@urkud
feat(topology/paracompact): define paracompact spaces (#6395)
0fa0d61 
Fixes #6391
@bors
Copy link

bors bot commented Mar 6, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/paracompact): define paracompact spaces [Merged by Bors] - feat(topology/paracompact): define paracompact spaces Mar 6, 2021
@bors bors bot closed this Mar 6, 2021
Partition of unity automation moved this from Reviewer approved to Done Mar 6, 2021
@bors bors bot deleted the paracompact branch March 6, 2021 13:32
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
@urkud @b-mehta
feat(topology/paracompact): define paracompact spaces (#6395)
5daf5c7 
Fixes #6391
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

@sgouezel sgouezel sgouezel left review comments

@jcommelin jcommelin jcommelin approved these changes

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
No open projects
Partition of unity
  
Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Define paracompact spaces
4 participants
@urkud @sgouezel @eric-wieser @jcommelin