Skip to content

[Merged by Bors] - feat: relative versions of equicontinuity#9286

Closed
ADedecker wants to merge 37 commits intomasterfrom
AD_equicontinuous_on
Closed

[Merged by Bors] - feat: relative versions of equicontinuity#9286
ADedecker wants to merge 37 commits intomasterfrom
AD_equicontinuous_on

Conversation

@ADedecker
Copy link
Copy Markdown
Member

@ADedecker ADedecker commented Dec 26, 2023 •
edited by Parcly-Taxel
Loading

@ADedecker ADedecker added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters labels Dec 26, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 26, 2023
@ADedecker ADedecker mentioned this pull request Dec 26, 2023
Closed
5 tasks
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 30, 2024
@ADedecker ADedecker added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 30, 2024
@ADedecker ADedecker added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 31, 2024
sgouezel
sgouezel reviewed Jan 31, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

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

LGTM, thanks!

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 31, 2024
ADedecker and others added 3 commits January 31, 2024 18:55
@ADedecker @sgouezel
Apply suggestions from code review
41ea5b3 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@ADedecker
More suggestions from review
bf6c307
@ADedecker
Long line
74683a6
@ADedecker ADedecker added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 31, 2024
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Feb 2, 2024

bors d+
(Do as you prefer on the closure vs closure' business, but maybe add some comment explaining the design).
Thanks!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 2, 2024

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

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Feb 2, 2024
@ADedecker ADedecker added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 2, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 2, 2024
@ADedecker
Copy link
Copy Markdown
Member Author

ADedecker commented Feb 2, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Feb 2, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 2, 2024
@ADedecker @hrmacbeth
feat: relative versions of equicontinuity (#9286)
935c079 
- [x] depends on: #7568



Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 2, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: relative versions of equicontinuity [Merged by Bors] - feat: relative versions of equicontinuity Feb 2, 2024
@mathlib-bors mathlib-bors bot closed this Feb 2, 2024
@mathlib-bors mathlib-bors bot deleted the AD_equicontinuous_on branch February 2, 2024 14:50
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. 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.

3 participants

@ADedecker @sgouezel @hrmacbeth