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(analysis/bounded_variation): some lemmas #18108

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(analysis/bounded_variation): some lemmas #18108

wants to merge 3 commits into from

Conversation

bottine
Copy link
Collaborator

@bottine bottine commented Jan 9, 2023

  • The variation of a function on a set is zero iff the image of the set has zero diameter.
  • Two functions that are pointwise at distance zero on a set have equal variation on that set.

Open in Gitpod

@bottine bottine added awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) labels Jan 9, 2023
sgouezel
sgouezel reviewed Jan 9, 2023
View reviewed changes
src/analysis/bounded_variation.lean Outdated Show resolved Hide resolved
src/analysis/bounded_variation.lean Outdated Show resolved Hide resolved
src/analysis/bounded_variation.lean Outdated Show resolved Hide resolved
src/analysis/bounded_variation.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel 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 9, 2023
@bottine bottine 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 9, 2023
@bottine
Copy link
Collaborator Author

bottine commented Jan 9, 2023

Thanks for the review/suggestions! I was kind of waiting for the CI to run to correct some of the style issues (since it was modifying a file quite low in the dependence chain).

@alreadydone alreadydone changed the title feat(analysis.bounded_variation): some lemmas feat(analysis/bounded_variation): some lemmas Jan 10, 2023
alreadydone
alreadydone approved these changes Jan 10, 2023
View reviewed changes
src/analysis/bounded_variation.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel 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 10, 2023
@bottine bottine 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 10, 2023
@bottine bottine requested a review from sgouezel January 10, 2023 10:44
@sgouezel
Copy link
Collaborator

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 Jan 10, 2023
bors bot pushed a commit that referenced this pull request Jan 10, 2023
@bottine
feat(analysis/bounded_variation): some lemmas (#18108)
a2d2e18 
* The variation of a function on a set is zero iff the image of the set has zero diameter.
* Two functions that are pointwise at distance zero on a set have equal variation on that set.
@bors
Copy link

bors bot commented Jan 10, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/bounded_variation): some lemmas [Merged by Bors] - feat(analysis/bounded_variation): some lemmas Jan 10, 2023
@bors bors bot closed this Jan 10, 2023
@bors bors bot deleted the bottine/analisys.bounded_variation/lemmas branch January 10, 2023 20:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone approved these changes

@sgouezel sgouezel Awaiting requested review from sgouezel

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+`.) t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@bottine @sgouezel @alreadydone