Zulip Chat Archive

Stream: maths

Topic: metric_space (fin n)


Daniel Roca González (Feb 05 2022 at 12:33):

Hi,

is there some reason against making docs#fin a metric space, with the distance inherited from nat? If simply nobody thought about that I would make a PR.

Kevin Buzzard (Feb 05 2022 at 12:37):

I can imagine that people might want a finite discrete metric space with n elements for which d(a,b)=1 if a!=b. So maybe you could make it but make it a def instead of an instance?

Reid Barton (Feb 05 2022 at 13:53):

I had the same first reaction but upon reflection I'm not sure how pertinent it is, because you could equally well want to put this 0-1 metric on an arbitrary type.

Daniel Roca González (Feb 05 2022 at 14:00):

Is there a way to "remove" an instance?

Yaël Dillies (Feb 05 2022 at 14:00):

local attribute [-instance] your_instance

Yaël Dillies (Feb 05 2022 at 14:01):

Reid Barton said:

I had the same first reaction but upon reflection I'm not sure how pertinent it is, because you could equally well want to put this 0-1 metric on an arbitrary type.

This calls for a discrete_metric type synonym, I suppose.

Daniel Roca González (Feb 05 2022 at 14:11):

Also different question but related: if we have an injective function a → b and b is a metric_space, is there a definition in mathlib of the pullback metric space structure on a?

Daniel Roca González (Feb 05 2022 at 14:12):

(That one should definitely not be an instance by default, but it could be a def)

Daniel Roca González (Feb 05 2022 at 14:12):

Yaël Dillies said:

local attribute [-instance] your_instance

thak you! that's what I wanted

Reid Barton (Feb 05 2022 at 14:13):

docs#metric_space.induced

Daniel Roca González (Feb 05 2022 at 14:23):

Turns out nat isn't a metric space either?

Kevin Buzzard (Feb 05 2022 at 14:24):

Perhaps for the same reason

Yury G. Kudryashov (Feb 05 2022 at 16:07):

int is a metric space. Note that you should make the metric_space structure compatible with the discrete topological_space structure.

Yury G. Kudryashov (Feb 05 2022 at 16:07):

(and introduce it near docs#nat.topological_space if this is not done yet)

Yury G. Kudryashov (Feb 05 2022 at 16:08):

Have a look at the way we define docs#int.metric_space


Last updated: Dec 20 2023 at 11:08 UTC