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: port Topology.MetricSpace.EMetricSpace #2407

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat: port Topology.MetricSpace.EMetricSpace #2407

wants to merge 8 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Feb 20, 2023 •
edited
Loading

@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from 719273f to 1db1758 Compare February 21, 2023 00:31
@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 22, 2023
@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from 967088d to f1467ff Compare February 25, 2023 00:46
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 25, 2023
@urkud urkud added the mathlib-port This is a port of a theory file from mathlib. label Feb 25, 2023
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR to Mathlib label Feb 25, 2023
@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from 8374533 to b8d7231 Compare February 25, 2023 20:19
@semorrison semorrison added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Feb 27, 2023
@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch 2 times, most recently from 3fca54a to 34bb65f Compare February 27, 2023 17:34
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 27, 2023
@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from 34bb65f to 7e12fc7 Compare February 27, 2023 17:35
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-review The author would like community review of the PR labels Feb 27, 2023
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR to Mathlib merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Feb 27, 2023
@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from 628278f to e592247 Compare February 28, 2023 05:35
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR to Mathlib and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. blocked-by-other-PR This PR depends on another PR to Mathlib labels Feb 28, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from e592247 to 0dd0edc Compare March 2, 2023 14:30
@urkud
feat: port Topology.MetricSpace.EmetricSpace
5fbb1fd
@urkud
Initial file copy from mathport
daf502a
@urkud
automated fixes
dcbbc54 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@urkud
Rename file
929bab0
@urkud
Search&replace
0ab687c 
* `HasEdist` -> `EDist`
* `Emetric` -> `EMetric`
* `nNReal` -> `nnreal`
@urkud
Snapshot
c3f4607
@urkud urkud force-pushed the port/Topology.MetricSpace.EmetricSpace branch from 0dd0edc to dc04de2 Compare March 3, 2023 04:01
@urkud urkud added the awaiting-review The author would like community review of the PR label Mar 3, 2023
jcommelin
jcommelin approved these changes Mar 3, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@bors
Copy link

bors bot commented Mar 3, 2023

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

@semorrison semorrison added delegated and removed awaiting-review The author would like community review of the PR labels Mar 3, 2023
@urkud
Copy link
Member Author

urkud commented Mar 3, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Mar 3, 2023
bors bot pushed a commit that referenced this pull request Mar 3, 2023
@urkud
feat: port Topology.MetricSpace.EMetricSpace (#2407)
0782bc7
@bors
Copy link

bors bot commented Mar 3, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Topology.MetricSpace.EMetricSpace [Merged by Bors] - feat: port Topology.MetricSpace.EMetricSpace Mar 3, 2023
@bors bors bot closed this Mar 3, 2023
@bors bors bot deleted the port/Topology.MetricSpace.EmetricSpace branch March 3, 2023 08:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@urkud @semorrison @jcommelin