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] - refactor(topology/metric_space/isometry): generalize to pseudo_metric #6910

Closed
wants to merge 20 commits into from
Closed

[Merged by Bors] - refactor(topology/metric_space/isometry): generalize to pseudo_metric #6910

wants to merge 20 commits into from

Conversation

riccardobrasca
Copy link
Member

@riccardobrasca riccardobrasca commented Mar 27, 2021 •
edited by github-actions bot

This is part of a series of PR to have the theory of semi_normed_group (and related concepts) in mathlib.

We generalize here isometry to pseudo_emetric_space and pseudo_metric_space.

Open in Gitpod

@riccardobrasca riccardobrasca added the awaiting-review The author would like community review of the PR label Mar 27, 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 Mar 27, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Mar 31, 2021
@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!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 31, 2021
@riccardobrasca riccardobrasca mentioned this pull request Mar 31, 2021
Closed
1 task
sgouezel
sgouezel reviewed Apr 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.

bors d+
Thanks!

src/topology/metric_space/isometry.lean Outdated Show resolved Hide resolved
src/topology/metric_space/isometry.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Apr 2, 2021

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

riccardobrasca and others added 2 commits April 2, 2021 22:39
@riccardobrasca @sgouezel
Update src/topology/metric_space/isometry.lean
86f4601 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@riccardobrasca @sgouezel
Update src/topology/metric_space/isometry.lean
4faa983 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@riccardobrasca
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 2, 2021
@riccardobrasca
refactor(topology/metric_space/isometry): generalize to pseudo_metric (
278ad33 
#6910)

This is part of a series of PR to have the theory of `semi_normed_group` (and related concepts) in mathlib.

We generalize here `isometry` to `pseudo_emetric_space` and `pseudo_metric_space`.
@bors
Copy link

bors bot commented Apr 3, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(topology/metric_space/isometry): generalize to pseudo_metric [Merged by Bors] - refactor(topology/metric_space/isometry): generalize to pseudo_metric Apr 3, 2021
@bors bors bot closed this Apr 3, 2021
@bors bors bot deleted the pseudo_isometry branch April 3, 2021 02:34
bors bot pushed a commit that referenced this pull request Apr 6, 2021
@riccardobrasca
refactor(analysis/normed_space/normed_group_hom): generalize to semi_…
82b0b30 
…normed_group (#6977)

This is part of a series of PR to have the theory of `semi_normed_group` (and related concepts) in mathlib.

We generalize here `normed_group_hom` to `semi_normed_group` (keeping the old name to avoid too long names).

- [x] depends on: #6910
@YaelDillies YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 17, 2021
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
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@riccardobrasca @sgouezel @YaelDillies