[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces #14315

winston-h-zhang · 2022-05-22T22:10:22Z

We define dilation α β as the type of maps that satisfy edist (f x) (f y) = r * edist x y for all x y. Here r : ℝ≥0, so we do not exclude the degenerate case of dilations which collapse into constant maps.

After this I will extend to {linear, affine}_dilation_{equiv}s and {linear, affine}_isometry_{equiv}s.

src/topology/metric_space/dilation.lean

winston-h-zhang · 2022-05-24T01:00:03Z

Thanks for the comments! I hope I've addressed everything

src/topology/metric_space/dilation.lean

winston-h-zhang · 2022-06-03T05:28:04Z

@jsm28 Please take a look at this again when you have the time! I've also requested Eric's review if you happen to be busy.

src/topology/metric_space/dilation.lean

… hzhang-dilations

winston-h-zhang · 2022-06-13T07:57:36Z

@eric-wieser @urkud, I've put up a new definition of dilation and ratio that is well-defined. I still have the existential inside the structure, then as Yury suggested I defined ratio with if ... then ... else. This actually went quite smoothly. Let me know what you guys think!

eric-wieser · 2022-09-01T05:32:10Z

I'm pretty short on time at the moment, I'm happy to let another maintainer take over

j-loreaux

Lots of suggestions, all relatively small. Some are important though. Among them:

typos
style issues
golfs
protecting names which conflict with ones in the root namespace (this is important)
a suggestion about splitting the existential in some hypotheses

After these are all fixed it should be ready for merging.

src/topology/metric_space/dilation.lean

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

urkud · 2023-06-09T15:24:01Z

@eric-wieser Should we merge it now?

eric-wieser · 2023-06-09T15:36:35Z

src/topology/metric_space/dilation.lean

+We define dilations, i.e., maps between emetric spaces that satisfy
+`edist (f x) (f y) = r * edist x y`.


This description is misleading because it doesn't allow r = 0 or r = \top. I think we should add an explanation of why we don't want to consider those cases in this module docstring.

j-loreaux · 2023-06-23T19:05:20Z

maintainer merge

github-actions · 2023-06-23T19:05:34Z

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

dupuisf · 2023-06-23T19:10:28Z

bors r+

) We define `dilation α β` as the type of maps that satisfy `edist (f x) (f y) = r * edist x y` for all `x y`. Here `r : ℝ≥0`, so we do not exclude the degenerate case of dilations which collapse into constant maps. After this I will extend to `{linear, affine}_dilation_{equiv}`s and `{linear, affine}_isometry_{equiv}`s. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: JovanGerb <jovan.gerbscheid@gmail.com>

bors · 2023-06-23T20:17:04Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

winston-h-zhang added 2 commits May 22, 2022 14:36

initial commit

9d72e4c

satisfy linter

0d4b86d

winston-h-zhang self-assigned this May 22, 2022

winston-h-zhang added the awaiting-review The author would like community review of the PR label May 22, 2022

satisfy linter again

7d0e3c6

winston-h-zhang requested a review from jsm28 May 22, 2022 22:19

bundle ratio

5227540

jsm28 reviewed May 23, 2022

View reviewed changes

src/topology/metric_space/dilation.lean Outdated Show resolved Hide resolved

jsm28 reviewed May 23, 2022

View reviewed changes

winston-h-zhang added 4 commits May 23, 2022 16:50

add suggestions

e68362c

fix doc-string

368a28f

fix: isometry to dilation

3279fd2

remove #print

3e9e60e

winston-h-zhang added 3 commits May 23, 2022 18:02

fix doc strings

a8a42ba

satisify linter

5e83302

oops linter again

7d991c1

winston-h-zhang requested a review from jsm28 May 25, 2022 16:31

jsm28 reviewed May 27, 2022

View reviewed changes

src/topology/metric_space/dilation.lean Outdated Show resolved Hide resolved

src/topology/metric_space/dilation.lean Outdated Show resolved Hide resolved

src/topology/metric_space/dilation.lean Outdated Show resolved Hide resolved

winston-h-zhang added 3 commits May 27, 2022 17:38

add suggestions from review

e1f703c

satisfy linter

2adeb37

header details

7b17162

winston-h-zhang requested a review from jsm28 May 31, 2022 16:34

winston-h-zhang requested a review from eric-wieser June 3, 2022 05:29

eric-wieser reviewed Jun 3, 2022

View reviewed changes

src/topology/metric_space/dilation.lean Outdated Show resolved Hide resolved

winston-h-zhang added 3 commits June 3, 2022 23:14

Merge branch 'master' of github.com:leanprover-community/mathlib into…

6f53494

… hzhang-dilations

r_pos, no exists

5d9cea2

new definition

36a0dd6

urkud added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters t-analysis Analysis (normed *, calculus) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 1, 2022

urkud unassigned eric-wieser Sep 1, 2022

j-loreaux self-assigned this Oct 4, 2022

j-loreaux reviewed Oct 4, 2022

View reviewed changes

j-loreaux 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 Oct 4, 2022

urkud and others added 2 commits November 5, 2022 01:25

Apply suggestions from code review

8154d26

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

fix errors

9189b50

urkud mentioned this pull request May 23, 2023

[Merged by Bors] - feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged #18990

Closed

urkud 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 Jun 8, 2023

eric-wieser reviewed Jun 9, 2023

View reviewed changes

urkud added 3 commits June 21, 2023 10:29

Merge branch 'master' into hzhang-dilations

20a9ae4

Add bibitem

75d9fd2

Add a paragraph to the module docstring.

f28b97f

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 Jun 23, 2023

bors bot changed the title ~~feat(topology/metric_space/dilation): Dilations on metric spaces~~ [Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces Jun 23, 2023

bors bot closed this Jun 23, 2023

bors bot deleted the hzhang-dilations branch June 23, 2023 20:17

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces #14315

[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces #14315

winston-h-zhang commented May 22, 2022 •

edited by alreadydone

Loading

winston-h-zhang commented May 24, 2022

winston-h-zhang commented Jun 3, 2022 •

edited

Loading

winston-h-zhang commented Jun 13, 2022 •

edited

Loading

eric-wieser commented Sep 1, 2022

j-loreaux left a comment

urkud commented Jun 9, 2023

eric-wieser Jun 9, 2023

j-loreaux commented Jun 23, 2023

github-actions bot commented Jun 23, 2023

dupuisf commented Jun 23, 2023

bors bot commented Jun 23, 2023

		We define dilations, i.e., maps between emetric spaces that satisfy
		`edist (f x) (f y) = r * edist x y`.

[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces #14315

[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces #14315

Conversation

winston-h-zhang commented May 22, 2022 • edited by alreadydone Loading

winston-h-zhang commented May 24, 2022

winston-h-zhang commented Jun 3, 2022 • edited Loading

winston-h-zhang commented Jun 13, 2022 • edited Loading

eric-wieser commented Sep 1, 2022

j-loreaux left a comment

Choose a reason for hiding this comment

urkud commented Jun 9, 2023

eric-wieser Jun 9, 2023

Choose a reason for hiding this comment

j-loreaux commented Jun 23, 2023

github-actions bot commented Jun 23, 2023

dupuisf commented Jun 23, 2023

bors bot commented Jun 23, 2023

winston-h-zhang commented May 22, 2022 •

edited by alreadydone

Loading

winston-h-zhang commented Jun 3, 2022 •

edited

Loading

winston-h-zhang commented Jun 13, 2022 •

edited

Loading