Skip to content

[Merged by Bors] - chore(Topology/MetricSpace/PseudoMetric): Split#13977

Closed
YaelDillies wants to merge 1 commit intomasterfrom
split_pseudo_metric
Closed

[Merged by Bors] - chore(Topology/MetricSpace/PseudoMetric): Split#13977
YaelDillies wants to merge 1 commit intomasterfrom
split_pseudo_metric

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jun 20, 2024

This reduces the long pole.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 272b1b0693

Import changes

No significant changes to the import graph

Declarations diff

+ dist_eq
+ dist_le_of_mem_pi_Icc
+ dist_up_up
+ for
+ instance : PseudoMetricSpace (Additive α) := ‹_›
+ instance : PseudoMetricSpace (Multiplicative α) := ‹_›
+ instance : PseudoMetricSpace (ULift β) := PseudoMetricSpace.induced ULift.down ‹_›
+ instance : PseudoMetricSpace αᵒᵈ := ‹_›
+ nndist_eq
+ nndist_up_up
++-- -/
- Real.dist_le_of_mem_pi_Icc
- ULift.dist_eq
- ULift.dist_up_up
- ULift.nndist_eq
- ULift.nndist_up_up
- instance : PseudoMetricSpace (ULift β)
- instance [PseudoMetricSpace X] : PseudoMetricSpace (Additive X) := ‹PseudoMetricSpace X›
- instance [PseudoMetricSpace X] : PseudoMetricSpace (Multiplicative X) := ‹PseudoMetricSpace X›
- instance [PseudoMetricSpace X] : PseudoMetricSpace Xᵒᵈ := ‹PseudoMetricSpace X›

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>

@YaelDillies YaelDillies mentioned this pull request Jun 20, 2024
Closed
@YaelDillies YaelDillies added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Jun 20, 2024
Ruben-VandeVelde
Ruben-VandeVelde reviewed Jun 20, 2024
View reviewed changes
@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 Jun 20, 2024
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 22, 2024
@grunweg grunweg mentioned this pull request Jun 23, 2024
Closed
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 23, 2024 •
edited
Loading

Let me cross-reference #14048 which tries the same. (I'll be happy to review either, but submitting my PhD thesis takes priority -> I may take about a week to get to this.)

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jun 23, 2024

Ah, a pity, I wish I'd seen this before duplicating the work. I'm perfectly happy to defer to Yael's version if they can fix the merge conflicts. (Although, the import analyzer does seem to rate mine epsilonically better. :-)

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jun 23, 2024

Wait sorry, which PR are you talking about, @grunweg ? You linked to this very PR.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 23, 2024

Wait sorry, which PR are you talking about, @grunweg ? You linked to this very PR.

Ah sorry, copy-paste fail :-) I've fixed the comment.

@YaelDillies YaelDillies force-pushed the split_pseudo_metric branch from 8a3b558 to 272b1b0 Compare June 23, 2024 20:32
@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 Jun 23, 2024
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jun 23, 2024

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2024
@YaelDillies
chore(Topology/MetricSpace/PseudoMetric): Split (#13977)
fca6b3a 
This reduces the long pole.
@adomani
Copy link
Copy Markdown
Contributor

adomani commented Jun 23, 2024

To add yet another comment: the diff here also had those stray structure-less "structure."!

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Topology/MetricSpace/PseudoMetric): Split [Merged by Bors] - chore(Topology/MetricSpace/PseudoMetric): Split Jun 23, 2024
@mathlib-bors mathlib-bors bot closed this Jun 23, 2024
@mathlib-bors mathlib-bors bot deleted the split_pseudo_metric branch June 23, 2024 22:55
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Jun 24, 2024

Oh sorry @semorrison I wanted to compare our two approaches to understand why your PR performs better on import changes. I merely merged master to check the new long pole. 🙈

kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@YaelDillies @kbuzzard
chore(Topology/MetricSpace/PseudoMetric): Split (#13977)
f975725 
This reduces the long pole.
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@YaelDillies @dagurtomas
chore(Topology/MetricSpace/PseudoMetric): Split (#13977)
71d021f 
This reduces the long pole.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees

No one assigned

Labels

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.

5 participants

@YaelDillies @grunweg @kim-em @adomani @Ruben-VandeVelde