Skip to content

[Merged by Bors] - feat: f⁻¹ is continuous iff f is#13951

Closed
YaelDillies wants to merge 2 commits intomasterfrom
continuous_inv_iff
Closed

[Merged by Bors] - feat: f⁻¹ is continuous iff f is#13951
YaelDillies wants to merge 2 commits intomasterfrom
continuous_inv_iff

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jun 19, 2024 •
edited
Loading

... and similar results for lipschitzness.

From LeanCamCombi

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review t-topology Topological spaces, uniform spaces, metric spaces, filters t-algebra Algebra (groups, rings, fields, etc) labels Jun 19, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 19, 2024 •
edited
Loading

PR summary 5a1648fddc

Import changes

No significant changes to the import graph

Declarations diff

+ antilipschitzWith_inv_iff
+ continuousAt_inv_iff
+ continuousOn_inv_iff
+ continuous_inv_iff
+ lipschitzOnWith_inv_iff
+ lipschitzWith_inv_iff
+ locallyLipschitz_inv_iff
+ ⟨AntilipschitzWith.of_inv,
+ ⟨Continuous.of_inv,
+ ⟨ContinuousAt.of_inv,
+ ⟨ContinuousOn.of_inv,
+ ⟨LipschitzOnWith.of_inv,
+ ⟨LipschitzWith.of_inv,
+ ⟨LocallyLipschitz.of_inv,
- inv

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

grunweg
grunweg reviewed Jun 19, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Seems reasonable to me - but somebody who knows this part of the library better should take a look as well.
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 19, 2024

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 19, 2024
sgouezel
sgouezel reviewed Jun 19, 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.

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 19, 2024

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 19, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jun 19, 2024

bors merge

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 19, 2024

Canceled.

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jun 19, 2024

Sorry, was too fast!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 19, 2024
@YaelDillies
feat: f⁻¹ is continuous iff f is (#13951)
63b99ca 
... and similar results for lipschitzness.

From LeanCamCombi
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: f⁻¹ is continuous iff f is [Merged by Bors] - feat: f⁻¹ is continuous iff f is Jun 19, 2024
@mathlib-bors mathlib-bors bot closed this Jun 19, 2024
@mathlib-bors mathlib-bors bot deleted the continuous_inv_iff branch June 19, 2024 14:17
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @AntoineChambert-Loir
feat: f⁻¹ is continuous iff f is (#13951)
ae1c0d4 
... and similar results for lipschitzness.

From LeanCamCombi
grunweg pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @grunweg
feat: f⁻¹ is continuous iff f is (#13951)
ba5d9c3 
... and similar results for lipschitzness.

From LeanCamCombi
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@YaelDillies @kbuzzard
feat: f⁻¹ is continuous iff f is (#13951)
c713db6 
... and similar results for lipschitzness.

From LeanCamCombi
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

@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). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc) 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

@YaelDillies @grunweg @sgouezel